Metamath Proof Explorer

Theorem adj1

Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adj1 
|- ( ( T e. dom adjh /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( ( adjh ` T ) ` A ) .ih B ) )

Proof

Step Hyp Ref Expression
1 funadj 
 |-  Fun adjh
2 funfvop 
 |-  ( ( Fun adjh /\ T e. dom adjh ) -> <. T , ( adjh ` T ) >. e. adjh )
3 1 2 mpan 
 |-  ( T e. dom adjh -> <. T , ( adjh ` T ) >. e. adjh )
4 dfadj2 
 |-  adjh = { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( z ` y ) ) = ( ( w ` x ) .ih y ) ) }
5 3 4 eleqtrdi 
 |-  ( T e. dom adjh -> <. T , ( adjh ` T ) >. e. { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( z ` y ) ) = ( ( w ` x ) .ih y ) ) } )
6 fvex 
 |-  ( adjh ` T ) e. _V
7 feq1 
 |-  ( z = T -> ( z : ~H --> ~H <-> T : ~H --> ~H ) )
8 fveq1 
 |-  ( z = T -> ( z ` y ) = ( T ` y ) )
9 8 oveq2d 
 |-  ( z = T -> ( x .ih ( z ` y ) ) = ( x .ih ( T ` y ) ) )
10 9 eqeq1d 
 |-  ( z = T -> ( ( x .ih ( z ` y ) ) = ( ( w ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( w ` x ) .ih y ) ) )
11 10 2ralbidv 
 |-  ( z = T -> ( A. x e. ~H A. y e. ~H ( x .ih ( z ` y ) ) = ( ( w ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( w ` x ) .ih y ) ) )
12 7 11 3anbi13d 
 |-  ( z = T -> ( ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( z ` y ) ) = ( ( w ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( w ` x ) .ih y ) ) ) )
13 feq1 
 |-  ( w = ( adjh ` T ) -> ( w : ~H --> ~H <-> ( adjh ` T ) : ~H --> ~H ) )
14 fveq1 
 |-  ( w = ( adjh ` T ) -> ( w ` x ) = ( ( adjh ` T ) ` x ) )
15 14 oveq1d 
 |-  ( w = ( adjh ` T ) -> ( ( w ` x ) .ih y ) = ( ( ( adjh ` T ) ` x ) .ih y ) )
16 15 eqeq2d 
 |-  ( w = ( adjh ` T ) -> ( ( x .ih ( T ` y ) ) = ( ( w ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) ) )
17 16 2ralbidv 
 |-  ( w = ( adjh ` T ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( w ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) ) )
18 13 17 3anbi23d 
 |-  ( w = ( adjh ` T ) -> ( ( T : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( w ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) ) ) )
19 12 18 opelopabg 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) e. _V ) -> ( <. T , ( adjh ` T ) >. e. { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( z ` y ) ) = ( ( w ` x ) .ih y ) ) } <-> ( T : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) ) ) )
20 6 19 mpan2 
 |-  ( T e. dom adjh -> ( <. T , ( adjh ` T ) >. e. { <. z , w >. | ( z : ~H --> ~H /\ w : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( z ` y ) ) = ( ( w ` x ) .ih y ) ) } <-> ( T : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) ) ) )
21 5 20 mpbid 
 |-  ( T e. dom adjh -> ( T : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) ) )
22 21 simp3d 
 |-  ( T e. dom adjh -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) )
23 oveq1 
 |-  ( x = A -> ( x .ih ( T ` y ) ) = ( A .ih ( T ` y ) ) )
24 fveq2 
 |-  ( x = A -> ( ( adjh ` T ) ` x ) = ( ( adjh ` T ) ` A ) )
25 24 oveq1d 
 |-  ( x = A -> ( ( ( adjh ` T ) ` x ) .ih y ) = ( ( ( adjh ` T ) ` A ) .ih y ) )
26 23 25 eqeq12d 
 |-  ( x = A -> ( ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) <-> ( A .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` A ) .ih y ) ) )
27 fveq2 
 |-  ( y = B -> ( T ` y ) = ( T ` B ) )
28 27 oveq2d 
 |-  ( y = B -> ( A .ih ( T ` y ) ) = ( A .ih ( T ` B ) ) )
29 oveq2 
 |-  ( y = B -> ( ( ( adjh ` T ) ` A ) .ih y ) = ( ( ( adjh ` T ) ` A ) .ih B ) )
30 28 29 eqeq12d 
 |-  ( y = B -> ( ( A .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` A ) .ih y ) <-> ( A .ih ( T ` B ) ) = ( ( ( adjh ` T ) ` A ) .ih B ) ) )
31 26 30 rspc2v 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) -> ( A .ih ( T ` B ) ) = ( ( ( adjh ` T ) ` A ) .ih B ) ) )
32 22 31 syl5com 
 |-  ( T e. dom adjh -> ( ( A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( ( adjh ` T ) ` A ) .ih B ) ) )
33 32 3impib 
 |-  ( ( T e. dom adjh /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( ( adjh ` T ) ` A ) .ih B ) )