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 𝐴 ) ↔ 𝐵 ∈ ℝ ) )