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

Definition df-aj 25863
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
) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u
) ( s `  y ) ) ) } )
Distinct variable group:    t, s, u, w, x, y

Detailed syntax breakdown of Definition df-aj
StepHypRef Expression
1 caj 25861 . 2  class  adj
2 vu . . 3  setvar  u
3 vw . . 3  setvar  w
4 cnv 25675 . . 3  class  NrmCVec
52cv 1397 . . . . . . 7  class  u
6 cba 25677 . . . . . . 7  class  BaseSet
75, 6cfv 5570 . . . . . 6  class  ( BaseSet `  u )
83cv 1397 . . . . . . 7  class  w
98, 6cfv 5570 . . . . . 6  class  ( BaseSet `  w )
10 vt . . . . . . 7  setvar  t
1110cv 1397 . . . . . 6  class  t
127, 9, 11wf 5566 . . . . 5  wff  t : ( BaseSet `  u ) --> ( BaseSet `  w )
13 vs . . . . . . 7  setvar  s
1413cv 1397 . . . . . 6  class  s
159, 7, 14wf 5566 . . . . 5  wff  s : ( BaseSet `  w ) --> ( BaseSet `  u )
16 vx . . . . . . . . . . 11  setvar  x
1716cv 1397 . . . . . . . . . 10  class  x
1817, 11cfv 5570 . . . . . . . . 9  class  ( t `
 x )
19 vy . . . . . . . . . 10  setvar  y
2019cv 1397 . . . . . . . . 9  class  y
21 cdip 25808 . . . . . . . . . 10  class  .iOLD
228, 21cfv 5570 . . . . . . . . 9  class  ( .iOLD `  w )
2318, 20, 22co 6270 . . . . . . . 8  class  ( ( t `  x ) ( .iOLD `  w ) y )
2420, 14cfv 5570 . . . . . . . . 9  class  ( s `
 y )
255, 21cfv 5570 . . . . . . . . 9  class  ( .iOLD `  u )
2617, 24, 25co 6270 . . . . . . . 8  class  ( x ( .iOLD `  u ) ( s `
 y ) )
2723, 26wceq 1398 . . . . . . 7  wff  ( ( t `  x ) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u
) ( s `  y ) )
2827, 19, 9wral 2804 . . . . . 6  wff  A. y  e.  ( BaseSet `  w )
( ( t `  x ) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u ) ( s `
 y ) )
2928, 16, 7wral 2804 . . . . 5  wff  A. x  e.  ( BaseSet `  u ) A. y  e.  ( BaseSet
`  w ) ( ( t `  x
) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u
) ( s `  y ) )
3012, 15, 29w3a 971 . . . 4  wff  ( t : ( BaseSet `  u
) --> ( BaseSet `  w
)  /\  s :
( BaseSet `  w ) --> ( BaseSet `  u )  /\  A. x  e.  (
BaseSet `  u ) A. y  e.  ( BaseSet `  w ) ( ( t `  x ) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u
) ( s `  y ) ) )
3130, 10, 13copab 4496 . . 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
) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u
) ( s `  y ) ) ) }
322, 3, 4, 4, 31cmpt2 6272 . 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 ) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u
) ( s `  y ) ) ) } )
331, 32wceq 1398 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
) ( .iOLD `  w ) y )  =  ( x ( .iOLD `  u
) ( s `  y ) ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  ajfval  25922
  Copyright terms: Public domain W3C validator