Metamath Proof Explorer

Theorem unopadj

Description: The inverse (converse) of a unitary operator is its adjoint. Equation 2 of AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unopadj 
|- ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih B ) = ( A .ih ( `' T ` B ) ) )

Proof

Step Hyp Ref Expression
1 unopf1o 
 |-  ( T e. UniOp -> T : ~H -1-1-onto-> ~H )
2 f1ocnvfv2 
 |-  ( ( T : ~H -1-1-onto-> ~H /\ B e. ~H ) -> ( T ` ( `' T ` B ) ) = B )
3 1 2 sylan 
 |-  ( ( T e. UniOp /\ B e. ~H ) -> ( T ` ( `' T ` B ) ) = B )
4 3 3adant2 
 |-  ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( T ` ( `' T ` B ) ) = B )
5 4 oveq2d 
 |-  ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih ( T ` ( `' T ` B ) ) ) = ( ( T ` A ) .ih B ) )
6 f1ocnv 
 |-  ( T : ~H -1-1-onto-> ~H -> `' T : ~H -1-1-onto-> ~H )
7 f1of 
 |-  ( `' T : ~H -1-1-onto-> ~H -> `' T : ~H --> ~H )
8 1 6 7 3syl 
 |-  ( T e. UniOp -> `' T : ~H --> ~H )
9 8 ffvelcdmda 
 |-  ( ( T e. UniOp /\ B e. ~H ) -> ( `' T ` B ) e. ~H )
10 9 3adant2 
 |-  ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( `' T ` B ) e. ~H )
11 unop 
 |-  ( ( T e. UniOp /\ A e. ~H /\ ( `' T ` B ) e. ~H ) -> ( ( T ` A ) .ih ( T ` ( `' T ` B ) ) ) = ( A .ih ( `' T ` B ) ) )
12 10 11 syld3an3 
 |-  ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih ( T ` ( `' T ` B ) ) ) = ( A .ih ( `' T ` B ) ) )
13 5 12 eqtr3d 
 |-  ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih B ) = ( A .ih ( `' T ` B ) ) )