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

Definition df-aj 22204
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 22202 . 2  class  adj
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 22016 . . 3  class  NrmCVec
52cv 1648 . . . . . . 7  class  u
6 cba 22018 . . . . . . 7  class  BaseSet
75, 6cfv 5413 . . . . . 6  class  ( BaseSet `  u )
83cv 1648 . . . . . . 7  class  w
98, 6cfv 5413 . . . . . 6  class  ( BaseSet `  w )
10 vt . . . . . . 7  set  t
1110cv 1648 . . . . . 6  class  t
127, 9, 11wf 5409 . . . . 5  wff  t : ( BaseSet `  u ) --> ( BaseSet `  w )
13 vs . . . . . . 7  set  s
1413cv 1648 . . . . . 6  class  s
159, 7, 14wf 5409 . . . . 5  wff  s : ( BaseSet `  w ) --> ( BaseSet `  u )
16 vx . . . . . . . . . . 11  set  x
1716cv 1648 . . . . . . . . . 10  class  x
1817, 11cfv 5413 . . . . . . . . 9  class  ( t `
 x )
19 vy . . . . . . . . . 10  set  y
2019cv 1648 . . . . . . . . 9  class  y
21 cdip 22149 . . . . . . . . . 10  class  .i OLD
228, 21cfv 5413 . . . . . . . . 9  class  ( .i
OLD `  w )
2318, 20, 22co 6040 . . . . . . . 8  class  ( ( t `  x ) ( .i OLD `  w
) y )
2420, 14cfv 5413 . . . . . . . . 9  class  ( s `
 y )
255, 21cfv 5413 . . . . . . . . 9  class  ( .i
OLD `  u )
2617, 24, 25co 6040 . . . . . . . 8  class  ( x ( .i OLD `  u
) ( s `  y ) )
2723, 26wceq 1649 . . . . . . 7  wff  ( ( t `  x ) ( .i OLD `  w
) y )  =  ( x ( .i
OLD `  u )
( s `  y
) )
2827, 19, 9wral 2666 . . . . . 6  wff  A. y  e.  ( BaseSet `  w )
( ( t `  x ) ( .i
OLD `  w )
y )  =  ( x ( .i OLD `  u ) ( s `
 y ) )
2928, 16, 7wral 2666 . . . . 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 936 . . . 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 4225 . . 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 6042 . 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 1649 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  22263
  Copyright terms: Public domain W3C validator