Metamath Proof Explorer

Theorem adj2

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

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

Proof

Step Hyp Ref Expression
1 adj1 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( B .ih ( T ` A ) ) = ( ( ( adjh ` T ) ` B ) .ih A ) )
2 simp2 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> B e. ~H )
3 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
4 3 ffvelcdmda 
 |-  ( ( T e. dom adjh /\ A e. ~H ) -> ( T ` A ) e. ~H )
5 4 3adant2 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( T ` A ) e. ~H )
6 ax-his1 
 |-  ( ( B e. ~H /\ ( T ` A ) e. ~H ) -> ( B .ih ( T ` A ) ) = ( * ` ( ( T ` A ) .ih B ) ) )
7 2 5 6 syl2anc 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( B .ih ( T ` A ) ) = ( * ` ( ( T ` A ) .ih B ) ) )
8 adjcl 
 |-  ( ( T e. dom adjh /\ B e. ~H ) -> ( ( adjh ` T ) ` B ) e. ~H )
9 8 3adant3 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( ( adjh ` T ) ` B ) e. ~H )
10 simp3 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> A e. ~H )
11 ax-his1 
 |-  ( ( ( ( adjh ` T ) ` B ) e. ~H /\ A e. ~H ) -> ( ( ( adjh ` T ) ` B ) .ih A ) = ( * ` ( A .ih ( ( adjh ` T ) ` B ) ) ) )
12 9 10 11 syl2anc 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( ( ( adjh ` T ) ` B ) .ih A ) = ( * ` ( A .ih ( ( adjh ` T ) ` B ) ) ) )
13 1 7 12 3eqtr3d 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( * ` ( ( T ` A ) .ih B ) ) = ( * ` ( A .ih ( ( adjh ` T ) ` B ) ) ) )
14 hicl 
 |-  ( ( ( T ` A ) e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih B ) e. CC )
15 5 2 14 syl2anc 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( ( T ` A ) .ih B ) e. CC )
16 hicl 
 |-  ( ( A e. ~H /\ ( ( adjh ` T ) ` B ) e. ~H ) -> ( A .ih ( ( adjh ` T ) ` B ) ) e. CC )
17 10 9 16 syl2anc 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( A .ih ( ( adjh ` T ) ` B ) ) e. CC )
18 cj11 
 |-  ( ( ( ( T ` A ) .ih B ) e. CC /\ ( A .ih ( ( adjh ` T ) ` B ) ) e. CC ) -> ( ( * ` ( ( T ` A ) .ih B ) ) = ( * ` ( A .ih ( ( adjh ` T ) ` B ) ) ) <-> ( ( T ` A ) .ih B ) = ( A .ih ( ( adjh ` T ) ` B ) ) ) )
19 15 17 18 syl2anc 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( ( * ` ( ( T ` A ) .ih B ) ) = ( * ` ( A .ih ( ( adjh ` T ) ` B ) ) ) <-> ( ( T ` A ) .ih B ) = ( A .ih ( ( adjh ` T ) ` B ) ) ) )
20 13 19 mpbid 
 |-  ( ( T e. dom adjh /\ B e. ~H /\ A e. ~H ) -> ( ( T ` A ) .ih B ) = ( A .ih ( ( adjh ` T ) ` B ) ) )
21 20 3com23 
 |-  ( ( T e. dom adjh /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih B ) = ( A .ih ( ( adjh ` T ) ` B ) ) )