Metamath Proof Explorer

Theorem unopadj2

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 ∈ UniOp → adj h ⁡ T = T -1

Proof

Step Hyp Ref Expression
1 unoplin ⊢ T ∈ UniOp → T ∈ LinOp
2 lnopf ⊢ T ∈ LinOp → T : ℋ ⟶ ℋ
3 1 2 syl ⊢ T ∈ UniOp → T : ℋ ⟶ ℋ
4 cnvunop ⊢ T ∈ UniOp → T -1 ∈ UniOp
5 unoplin ⊢ T -1 ∈ UniOp → T -1 ∈ LinOp
6 lnopf ⊢ T -1 ∈ LinOp → T -1 : ℋ ⟶ ℋ
7 4 5 6 3syl ⊢ T ∈ UniOp → T -1 : ℋ ⟶ ℋ
8 unopadj ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih T -1 ⁡ y
9 8 3expib ⊢ T ∈ UniOp → x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih T -1 ⁡ y
10 9 ralrimivv ⊢ T ∈ UniOp → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih T -1 ⁡ y
11 adjeq ⊢ T : ℋ ⟶ ℋ ∧ T -1 : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih T -1 ⁡ y → adj h ⁡ T = T -1
12 3 7 10 11 syl3anc ⊢ T ∈ UniOp → adj h ⁡ T = T -1