Metamath Proof Explorer

Theorem adjeq

Description: A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjeq 
|- ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) -> ( adjh ` T ) = S )

Proof

Step Hyp Ref Expression
1 funadj 
 |-  Fun adjh
2 df-adjh 
 |-  adjh = { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( z ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) }
3 2 eleq2i 
 |-  ( <. T , S >. e. adjh <-> <. T , S >. e. { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( z ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) } )
4 ax-hilex 
 |-  ~H e. _V
5 fex 
 |-  ( ( T : ~H --> ~H /\ ~H e. _V ) -> T e. _V )
6 4 5 mpan2 
 |-  ( T : ~H --> ~H -> T e. _V )
7 fex 
 |-  ( ( S : ~H --> ~H /\ ~H e. _V ) -> S e. _V )
8 4 7 mpan2 
 |-  ( S : ~H --> ~H -> S e. _V )
9 feq1 
 |-  ( z = T -> ( z : ~H --> ~H <-> T : ~H --> ~H ) )
10 fveq1 
 |-  ( z = T -> ( z ` x ) = ( T ` x ) )
11 10 oveq1d 
 |-  ( z = T -> ( ( z ` x ) .ih y ) = ( ( T ` x ) .ih y ) )
12 11 eqeq1d 
 |-  ( z = T -> ( ( ( z ` x ) .ih y ) = ( x .ih ( w ` y ) ) <-> ( ( T ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) )
13 12 2ralbidv 
 |-  ( z = T -> ( A. x e. ~H A. y e. ~H ( ( z ` x ) .ih y ) = ( x .ih ( w ` y ) ) <-> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) )
14 9 13 3anbi13d 
 |-  ( z = T -> ( ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( z ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) <-> ( T : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) ) )
15 feq1 
 |-  ( w = S -> ( w : ~H --> ~H <-> S : ~H --> ~H ) )
16 fveq1 
 |-  ( w = S -> ( w ` y ) = ( S ` y ) )
17 16 oveq2d 
 |-  ( w = S -> ( x .ih ( w ` y ) ) = ( x .ih ( S ` y ) ) )
18 17 eqeq2d 
 |-  ( w = S -> ( ( ( T ` x ) .ih y ) = ( x .ih ( w ` y ) ) <-> ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) )
19 18 2ralbidv 
 |-  ( w = S -> ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( w ` y ) ) <-> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) )
20 15 19 3anbi23d 
 |-  ( w = S -> ( ( T : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) <-> ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) ) )
21 14 20 opelopabg 
 |-  ( ( T e. _V /\ S e. _V ) -> ( <. T , S >. e. { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( z ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) } <-> ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) ) )
22 6 8 21 syl2an 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H ) -> ( <. T , S >. e. { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( z ` x ) .ih y ) = ( x .ih ( w ` y ) ) ) } <-> ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) ) )
23 3 22 syl5bb 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H ) -> ( <. T , S >. e. adjh <-> ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) ) )
24 df-3an 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) <-> ( ( T : ~H --> ~H /\ S : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) )
25 24 baibr 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) <-> ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) ) )
26 23 25 bitr4d 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H ) -> ( <. T , S >. e. adjh <-> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) )
27 26 biimp3ar 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) -> <. T , S >. e. adjh )
28 funopfv 
 |-  ( Fun adjh -> ( <. T , S >. e. adjh -> ( adjh ` T ) = S ) )
29 1 27 28 mpsyl 
 |-  ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) -> ( adjh ` T ) = S )