Metamath Proof Explorer

Theorem unopadj

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 ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih B = A ⋅ ih T -1 ⁡ B

Proof

Step Hyp Ref Expression
1 unopf1o ⊢ T ∈ UniOp → T : ℋ ⟶ 1-1 onto ℋ
2 f1ocnvfv2 ⊢ T : ℋ ⟶ 1-1 onto ℋ ∧ B ∈ ℋ → T ⁡ T -1 ⁡ B = B
3 1 2 sylan ⊢ T ∈ UniOp ∧ B ∈ ℋ → T ⁡ T -1 ⁡ B = B
4 3 3adant2 ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ T -1 ⁡ B = B
5 4 oveq2d ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih T ⁡ T -1 ⁡ B = T ⁡ A ⋅ ih B
6 f1ocnv ⊢ T : ℋ ⟶ 1-1 onto ℋ → T -1 : ℋ ⟶ 1-1 onto ℋ
7 f1of ⊢ T -1 : ℋ ⟶ 1-1 onto ℋ → T -1 : ℋ ⟶ ℋ
8 1 6 7 3syl ⊢ T ∈ UniOp → T -1 : ℋ ⟶ ℋ
9 8 ffvelcdmda ⊢ T ∈ UniOp ∧ B ∈ ℋ → T -1 ⁡ B ∈ ℋ
10 9 3adant2 ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T -1 ⁡ B ∈ ℋ
11 unop ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ T -1 ⁡ B ∈ ℋ → T ⁡ A ⋅ ih T ⁡ T -1 ⁡ B = A ⋅ ih T -1 ⁡ B
12 10 11 syld3an3 ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih T ⁡ T -1 ⁡ B = A ⋅ ih T -1 ⁡ B
13 5 12 eqtr3d ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih B = A ⋅ ih T -1 ⁡ B