Metamath Proof Explorer

Definition df-aj

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.)

Ref Expression
Assertion 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 caj 
 |-  adj
1 vu 
 |-  u
2 cnv 
 |-  NrmCVec
3 vw 
 |-  w
4 vt 
 |-  t
5 vs 
 |-  s
6 4 cv 
 |-  t
7 cba 
 |-  BaseSet
8 1 cv 
 |-  u
9 8 7 cfv 
 |-  ( BaseSet ` u )
10 3 cv 
 |-  w
11 10 7 cfv 
 |-  ( BaseSet ` w )
12 9 11 6 wf 
 |-  t : ( BaseSet ` u ) --> ( BaseSet ` w )
13 5 cv 
 |-  s
14 11 9 13 wf 
 |-  s : ( BaseSet ` w ) --> ( BaseSet ` u )
15 vx 
 |-  x
16 vy 
 |-  y
17 15 cv 
 |-  x
18 17 6 cfv 
 |-  ( t ` x )
19 cdip 
 |-  .iOLD
20 10 19 cfv 
 |-  ( .iOLD ` w )
21 16 cv 
 |-  y
22 18 21 20 co 
 |-  ( ( t ` x ) ( .iOLD ` w ) y )
23 8 19 cfv 
 |-  ( .iOLD ` u )
24 21 13 cfv 
 |-  ( s ` y )
25 17 24 23 co 
 |-  ( x ( .iOLD ` u ) ( s ` y ) )
26 22 25 wceq 
 |-  ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) )
27 26 16 11 wral 
 |-  A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) )
28 27 15 9 wral 
 |-  A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) )
29 12 14 28 w3a 
 |-  ( 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 ) ) )
30 29 4 5 copab 
 |-  { <. 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 ) ) ) }
31 1 3 2 2 30 cmpo 
 |-  ( 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 ) ) ) } )
32 0 31 wceq 
 |-  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 ) ) ) } )