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

Definition df-aj 21253
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 21251 . 2  class  adj
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 21065 . . 3  class  NrmCVec
52cv 1618 . . . . . . 7  class  u
6 cba 21067 . . . . . . 7  class  BaseSet
75, 6cfv 4638 . . . . . 6  class  ( BaseSet `  u )
83cv 1618 . . . . . . 7  class  w
98, 6cfv 4638 . . . . . 6  class  ( BaseSet `  w )
10 vt . . . . . . 7  set  t
1110cv 1618 . . . . . 6  class  t
127, 9, 11wf 4634 . . . . 5  wff  t : ( BaseSet `  u ) --> ( BaseSet `  w )
13 vs . . . . . . 7  set  s
1413cv 1618 . . . . . 6  class  s
159, 7, 14wf 4634 . . . . 5  wff  s : ( BaseSet `  w ) --> ( BaseSet `  u )
16 vx . . . . . . . . . . 11  set  x
1716cv 1618 . . . . . . . . . 10  class  x
1817, 11cfv 4638 . . . . . . . . 9  class  ( t `
 x )
19 vy . . . . . . . . . 10  set  y
2019cv 1618 . . . . . . . . 9  class  y
21 cdip 21198 . . . . . . . . . 10  class  .i OLD
228, 21cfv 4638 . . . . . . . . 9  class  ( .i
OLD `  w )
2318, 20, 22co 5757 . . . . . . . 8  class  ( ( t `  x ) ( .i OLD `  w
) y )
2420, 14cfv 4638 . . . . . . . . 9  class  ( s `
 y )
255, 21cfv 4638 . . . . . . . . 9  class  ( .i
OLD `  u )
2617, 24, 25co 5757 . . . . . . . 8  class  ( x ( .i OLD `  u
) ( s `  y ) )
2723, 26wceq 1619 . . . . . . 7  wff  ( ( t `  x ) ( .i OLD `  w
) y )  =  ( x ( .i
OLD `  u )
( s `  y
) )
2827, 19, 9wral 2516 . . . . . 6  wff  A. y  e.  ( BaseSet `  w )
( ( t `  x ) ( .i
OLD `  w )
y )  =  ( x ( .i OLD `  u ) ( s `
 y ) )
2928, 16, 7wral 2516 . . . . 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 939 . . . 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 4016 . . 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 5759 . 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 1619 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  21312
  Copyright terms: Public domain W3C validator