# 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
Assertion unopadj2 ${⊢}{T}\in \mathrm{UniOp}\to {adj}_{h}\left({T}\right)={{T}}^{-1}$

### Proof

Step Hyp Ref Expression
1 unoplin ${⊢}{T}\in \mathrm{UniOp}\to {T}\in \mathrm{LinOp}$
2 lnopf ${⊢}{T}\in \mathrm{LinOp}\to {T}:ℋ⟶ℋ$
3 1 2 syl ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ⟶ℋ$
4 cnvunop ${⊢}{T}\in \mathrm{UniOp}\to {{T}}^{-1}\in \mathrm{UniOp}$
5 unoplin ${⊢}{{T}}^{-1}\in \mathrm{UniOp}\to {{T}}^{-1}\in \mathrm{LinOp}$
6 lnopf ${⊢}{{T}}^{-1}\in \mathrm{LinOp}\to {{T}}^{-1}:ℋ⟶ℋ$
7 4 5 6 3syl ${⊢}{T}\in \mathrm{UniOp}\to {{T}}^{-1}:ℋ⟶ℋ$
8 unopadj ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({y}\right)$
9 8 3expib ${⊢}{T}\in \mathrm{UniOp}\to \left(\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({y}\right)\right)$
10 9 ralrimivv ${⊢}{T}\in \mathrm{UniOp}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({y}\right)$
11 adjeq ${⊢}\left({T}:ℋ⟶ℋ\wedge {{T}}^{-1}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({y}\right)\right)\to {adj}_{h}\left({T}\right)={{T}}^{-1}$
12 3 7 10 11 syl3anc ${⊢}{T}\in \mathrm{UniOp}\to {adj}_{h}\left({T}\right)={{T}}^{-1}$