MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-aj Unicode version

Definition df-aj 21328
Description: Define the adjoint of an operator (if it exists). The domain of  U adj W is the set of all operators from  U to  W that have an adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't require that  U and  W be Hilbert spaces nor that the operators be linear. Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-aj  |-  adj  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  { <. t ,  s >.  |  ( t : ( BaseSet `  u ) --> ( BaseSet `  w )  /\  s : ( BaseSet `  w
) --> ( BaseSet `  u
)  /\  A. x  e.  ( BaseSet `  u ) A. y  e.  ( BaseSet
`  w ) ( ( t `  x
) ( .i OLD `  w ) y )  =  ( x ( .i OLD `  u
) ( s `  y ) ) ) } )
Distinct variable group:    t, s, u, w, x, y

Detailed syntax breakdown of Definition df-aj
StepHypRef Expression
1 caj 21326 . 2  class  adj
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 21140 . . 3  class  NrmCVec
52cv 1622 . . . . . . 7  class  u
6 cba 21142 . . . . . . 7  class  BaseSet
75, 6cfv 5255 . . . . . 6  class  ( BaseSet `  u )
83cv 1622 . . . . . . 7  class  w
98, 6cfv 5255 . . . . . 6  class  ( BaseSet `  w )
10 vt . . . . . . 7  set  t
1110cv 1622 . . . . . 6  class  t
127, 9, 11wf 5251 . . . . 5  wff  t : ( BaseSet `  u ) --> ( BaseSet `  w )
13 vs . . . . . . 7  set  s
1413cv 1622 . . . . . 6  class  s
159, 7, 14wf 5251 . . . . 5  wff  s : ( BaseSet `  w ) --> ( BaseSet `  u )
16 vx . . . . . . . . . . 11  set  x
1716cv 1622 . . . . . . . . . 10  class  x
1817, 11cfv 5255 . . . . . . . . 9  class  ( t `
 x )
19 vy . . . . . . . . . 10  set  y
2019cv 1622 . . . . . . . . 9  class  y
21 cdip 21273 . . . . . . . . . 10  class  .i OLD
228, 21cfv 5255 . . . . . . . . 9  class  ( .i
OLD `  w )
2318, 20, 22co 5858 . . . . . . . 8  class  ( ( t `  x ) ( .i OLD `  w
) y )
2420, 14cfv 5255 . . . . . . . . 9  class  ( s `
 y )
255, 21cfv 5255 . . . . . . . . 9  class  ( .i
OLD `  u )
2617, 24, 25co 5858 . . . . . . . 8  class  ( x ( .i OLD `  u
) ( s `  y ) )
2723, 26wceq 1623 . . . . . . 7  wff  ( ( t `  x ) ( .i OLD `  w
) y )  =  ( x ( .i
OLD `  u )
( s `  y
) )
2827, 19, 9wral 2543 . . . . . 6  wff  A. y  e.  ( BaseSet `  w )
( ( t `  x ) ( .i
OLD `  w )
y )  =  ( x ( .i OLD `  u ) ( s `
 y ) )
2928, 16, 7wral 2543 . . . . 5  wff  A. x  e.  ( BaseSet `  u ) A. y  e.  ( BaseSet
`  w ) ( ( t `  x
) ( .i OLD `  w ) y )  =  ( x ( .i OLD `  u
) ( s `  y ) )
3012, 15, 29w3a 934 . . . 4  wff  ( t : ( BaseSet `  u
) --> ( BaseSet `  w
)  /\  s :
( BaseSet `  w ) --> ( BaseSet `  u )  /\  A. x  e.  (
BaseSet `  u ) A. y  e.  ( BaseSet `  w ) ( ( t `  x ) ( .i OLD `  w
) y )  =  ( x ( .i
OLD `  u )
( s `  y
) ) )
3130, 10, 13copab 4076 . . 3  class  { <. t ,  s >.  |  ( t : ( BaseSet `  u ) --> ( BaseSet `  w )  /\  s : ( BaseSet `  w
) --> ( BaseSet `  u
)  /\  A. x  e.  ( BaseSet `  u ) A. y  e.  ( BaseSet
`  w ) ( ( t `  x
) ( .i OLD `  w ) y )  =  ( x ( .i OLD `  u
) ( s `  y ) ) ) }
322, 3, 4, 4, 31cmpt2 5860 . 2  class  ( u  e.  NrmCVec ,  w  e.  NrmCVec 
|->  { <. t ,  s
>.  |  ( t : ( BaseSet `  u
) --> ( BaseSet `  w
)  /\  s :
( BaseSet `  w ) --> ( BaseSet `  u )  /\  A. x  e.  (
BaseSet `  u ) A. y  e.  ( BaseSet `  w ) ( ( t `  x ) ( .i OLD `  w
) y )  =  ( x ( .i
OLD `  u )
( s `  y
) ) ) } )
331, 32wceq 1623 1  wff  adj  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  { <. t ,  s >.  |  ( t : ( BaseSet `  u ) --> ( BaseSet `  w )  /\  s : ( BaseSet `  w
) --> ( BaseSet `  u
)  /\  A. x  e.  ( BaseSet `  u ) A. y  e.  ( BaseSet
`  w ) ( ( t `  x
) ( .i OLD `  w ) y )  =  ( x ( .i OLD `  u
) ( s `  y ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  ajfval  21387
  Copyright terms: Public domain W3C validator