Metamath Proof Explorer

Theorem hmopadj

Description: A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopadj ⊢ T ∈ HrmOp → adj h ⁡ T = T

Proof

Step Hyp Ref Expression
1 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
2 hmop ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
3 2 eqcomd ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih T ⁡ y
4 3 3expib ⊢ T ∈ HrmOp → x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih T ⁡ y
5 4 ralrimivv ⊢ T ∈ HrmOp → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih T ⁡ y
6 adjeq ⊢ T : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih T ⁡ y → adj h ⁡ T = T
7 1 1 5 6 syl3anc ⊢ T ∈ HrmOp → adj h ⁡ T = T