Metamath Proof Explorer

Theorem eighmre

Description: The eigenvalues of a Hermitian operator are real. Equation 1.30 of Hughes p. 49. (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eighmre ⊢ T ∈ HrmOp ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
2 eleigveccl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → A ∈ ℋ
3 eigvalcl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A ∈ ℂ
4 2 3 jca ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → A ∈ ℋ ∧ eigval ⁡ T ⁡ A ∈ ℂ
5 eigvec1 ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → T ⁡ A = eigval ⁡ T ⁡ A ⋅ ℎ A ∧ A ≠ 0 ℎ
6 4 5 jca ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → A ∈ ℋ ∧ eigval ⁡ T ⁡ A ∈ ℂ ∧ T ⁡ A = eigval ⁡ T ⁡ A ⋅ ℎ A ∧ A ≠ 0 ℎ
7 1 6 sylan ⊢ T ∈ HrmOp ∧ A ∈ eigvec ⁡ T → A ∈ ℋ ∧ eigval ⁡ T ⁡ A ∈ ℂ ∧ T ⁡ A = eigval ⁡ T ⁡ A ⋅ ℎ A ∧ A ≠ 0 ℎ
8 2 2 jca ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → A ∈ ℋ ∧ A ∈ ℋ
9 1 8 sylan ⊢ T ∈ HrmOp ∧ A ∈ eigvec ⁡ T → A ∈ ℋ ∧ A ∈ ℋ
10 hmop ⊢ T ∈ HrmOp ∧ A ∈ ℋ ∧ A ∈ ℋ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
11 10 3expb ⊢ T ∈ HrmOp ∧ A ∈ ℋ ∧ A ∈ ℋ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
12 9 11 syldan ⊢ T ∈ HrmOp ∧ A ∈ eigvec ⁡ T → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
13 eigre ⊢ A ∈ ℋ ∧ eigval ⁡ T ⁡ A ∈ ℂ ∧ T ⁡ A = eigval ⁡ T ⁡ A ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A ↔ eigval ⁡ T ⁡ A ∈ ℝ
14 13 biimpa ⊢ A ∈ ℋ ∧ eigval ⁡ T ⁡ A ∈ ℂ ∧ T ⁡ A = eigval ⁡ T ⁡ A ⋅ ℎ A ∧ A ≠ 0 ℎ ∧ A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A → eigval ⁡ T ⁡ A ∈ ℝ
15 7 12 14 syl2anc ⊢ T ∈ HrmOp ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A ∈ ℝ