Metamath Proof Explorer

Theorem hmopre

Description: The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopre ⊢ T ∈ HrmOp ∧ A ∈ ℋ → T ⁡ A ⋅ ih A ∈ ℝ

Proof

Step Hyp Ref Expression
1 hmop ⊢ T ∈ HrmOp ∧ A ∈ ℋ ∧ A ∈ ℋ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
2 1 3anidm23 ⊢ T ∈ HrmOp ∧ A ∈ ℋ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
3 2 eqcomd ⊢ T ∈ HrmOp ∧ A ∈ ℋ → T ⁡ A ⋅ ih A = A ⋅ ih T ⁡ A
4 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
5 4 ffvelrnda ⊢ T ∈ HrmOp ∧ A ∈ ℋ → T ⁡ A ∈ ℋ
6 hire ⊢ T ⁡ A ∈ ℋ ∧ A ∈ ℋ → T ⁡ A ⋅ ih A ∈ ℝ ↔ T ⁡ A ⋅ ih A = A ⋅ ih T ⁡ A
7 5 6 sylancom ⊢ T ∈ HrmOp ∧ A ∈ ℋ → T ⁡ A ⋅ ih A ∈ ℝ ↔ T ⁡ A ⋅ ih A = A ⋅ ih T ⁡ A
8 3 7 mpbird ⊢ T ∈ HrmOp ∧ A ∈ ℋ → T ⁡ A ⋅ ih A ∈ ℝ