# Metamath Proof Explorer

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
`|- ( 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 )`
` |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( `' T ` y ) ) )`
` |-  ( T e. UniOp -> ( ( x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( `' T ` y ) ) ) )`
` |-  ( T e. UniOp -> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( `' T ` y ) ) )`
` |-  ( ( 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 )`
` |-  ( T e. UniOp -> ( adjh ` T ) = `' T )`