# Metamath Proof Explorer

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