Metamath Proof Explorer

Theorem eigrei

Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for an eigenvalue B to be real. Generalization of Equation 1.30 of Hughes p. 49. (Contributed by NM, 21-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses eigre.1 ⊢ A ∈ ℋ
eigre.2 ⊢ B ∈ ℂ
Assertion eigrei ⊢ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A ↔ B ∈ ℝ

Proof

Step Hyp Ref Expression
1 eigre.1 ⊢ A ∈ ℋ
2 eigre.2 ⊢ B ∈ ℂ
3 oveq2 ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih T ⁡ A = A ⋅ ih B ⋅ ℎ A
4 his5 ⊢ B ∈ ℂ ∧ A ∈ ℋ ∧ A ∈ ℋ → A ⋅ ih B ⋅ ℎ A = B ‾ ⁢ A ⋅ ih A
5 2 1 1 4 mp3an ⊢ A ⋅ ih B ⋅ ℎ A = B ‾ ⁢ A ⋅ ih A
6 3 5 eqtrdi ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih T ⁡ A = B ‾ ⁢ A ⋅ ih A
7 oveq1 ⊢ T ⁡ A = B ⋅ ℎ A → T ⁡ A ⋅ ih A = B ⋅ ℎ A ⋅ ih A
8 ax-his3 ⊢ B ∈ ℂ ∧ A ∈ ℋ ∧ A ∈ ℋ → B ⋅ ℎ A ⋅ ih A = B ⁢ A ⋅ ih A
9 2 1 1 8 mp3an ⊢ B ⋅ ℎ A ⋅ ih A = B ⁢ A ⋅ ih A
10 7 9 eqtrdi ⊢ T ⁡ A = B ⋅ ℎ A → T ⁡ A ⋅ ih A = B ⁢ A ⋅ ih A
11 6 10 eqeq12d ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A ↔ B ‾ ⁢ A ⋅ ih A = B ⁢ A ⋅ ih A
12 1 1 hicli ⊢ A ⋅ ih A ∈ ℂ
13 ax-his4 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < A ⋅ ih A
14 1 13 mpan ⊢ A ≠ 0 ℎ → 0 < A ⋅ ih A
15 14 gt0ne0d ⊢ A ≠ 0 ℎ → A ⋅ ih A ≠ 0
16 2 cjcli ⊢ B ‾ ∈ ℂ
17 mulcan2 ⊢ B ‾ ∈ ℂ ∧ B ∈ ℂ ∧ A ⋅ ih A ∈ ℂ ∧ A ⋅ ih A ≠ 0 → B ‾ ⁢ A ⋅ ih A = B ⁢ A ⋅ ih A ↔ B ‾ = B
18 16 2 17 mp3an12 ⊢ A ⋅ ih A ∈ ℂ ∧ A ⋅ ih A ≠ 0 → B ‾ ⁢ A ⋅ ih A = B ⁢ A ⋅ ih A ↔ B ‾ = B
19 12 15 18 sylancr ⊢ A ≠ 0 ℎ → B ‾ ⁢ A ⋅ ih A = B ⁢ A ⋅ ih A ↔ B ‾ = B
20 11 19 sylan9bb ⊢ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A ↔ B ‾ = B
21 2 cjrebi ⊢ B ∈ ℝ ↔ B ‾ = B
22 20 21 bitr4di ⊢ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A ↔ B ∈ ℝ