This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℋ
eigre.2 ⊢ 𝐵 ∈ ℂ
Assertion eigrei ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐵 ·ℎ 𝐴 ) ∧ 𝐴 ≠ 0ℎ ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) ↔ 𝐵 ∈ ℝ ) )

Proof

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