Metamath Proof Explorer

Theorem unopadj2

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

Ref Expression
Assertion unopadj2 
|- ( T e. UniOp -> ( adjh ` T ) = `' T )

Proof

Step Hyp Ref Expression
1 unoplin 
 |-  ( T e. UniOp -> T e. LinOp )
2 lnopf 
 |-  ( T e. LinOp -> T : ~H --> ~H )
3 1 2 syl 
 |-  ( T e. UniOp -> T : ~H --> ~H )
4 cnvunop 
 |-  ( T e. UniOp -> `' T e. UniOp )
5 unoplin 
 |-  ( `' T e. UniOp -> `' T e. LinOp )
6 lnopf 
 |-  ( `' T e. LinOp -> `' T : ~H --> ~H )
7 4 5 6 3syl 
 |-  ( T e. UniOp -> `' T : ~H --> ~H )
8 unopadj 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( `' T ` y ) ) )
9 8 3expib 
 |-  ( T e. UniOp -> ( ( x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( `' T ` y ) ) ) )
10 9 ralrimivv 
 |-  ( T e. UniOp -> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( `' T ` y ) ) )
11 adjeq 
 |-  ( ( T : ~H --> ~H /\ `' T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( `' T ` y ) ) ) -> ( adjh ` T ) = `' T )
12 3 7 10 11 syl3anc 
 |-  ( T e. UniOp -> ( adjh ` T ) = `' T )