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
Assertion unopadj ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({B}\right)$

Proof

Step Hyp Ref Expression
1 unopf1o ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{1-1 onto}{⟶}ℋ$
2 f1ocnvfv2 ${⊢}\left({T}:ℋ\underset{1-1 onto}{⟶}ℋ\wedge {B}\in ℋ\right)\to {T}\left({{T}}^{-1}\left({B}\right)\right)={B}$
3 1 2 sylan ${⊢}\left({T}\in \mathrm{UniOp}\wedge {B}\in ℋ\right)\to {T}\left({{T}}^{-1}\left({B}\right)\right)={B}$
4 3 3adant2 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({{T}}^{-1}\left({B}\right)\right)={B}$
5 4 oveq2d ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({{T}}^{-1}\left({B}\right)\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}$
6 f1ocnv ${⊢}{T}:ℋ\underset{1-1 onto}{⟶}ℋ\to {{T}}^{-1}:ℋ\underset{1-1 onto}{⟶}ℋ$
7 f1of ${⊢}{{T}}^{-1}:ℋ\underset{1-1 onto}{⟶}ℋ\to {{T}}^{-1}:ℋ⟶ℋ$
8 1 6 7 3syl ${⊢}{T}\in \mathrm{UniOp}\to {{T}}^{-1}:ℋ⟶ℋ$
9 8 ffvelrnda ${⊢}\left({T}\in \mathrm{UniOp}\wedge {B}\in ℋ\right)\to {{T}}^{-1}\left({B}\right)\in ℋ$
10 9 3adant2 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {{T}}^{-1}\left({B}\right)\in ℋ$
11 unop ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {{T}}^{-1}\left({B}\right)\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({{T}}^{-1}\left({B}\right)\right)={A}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({B}\right)$
12 10 11 syld3an3 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({{T}}^{-1}\left({B}\right)\right)={A}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({B}\right)$
13 5 12 eqtr3d ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({B}\right)$