Metamath Proof Explorer

Theorem eigre

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, 19-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigre ⊢A∈ℋ∧B∈ℂ∧T⁡A=B⋅ℎA∧A≠0ℎ→A⋅ihT⁡A=T⁡A⋅ihA↔B∈ℝ

Proof

Step Hyp Ref Expression
1 fveq2 ⊢A=ifA∈ℋA0ℎ→T⁡A=T⁡ifA∈ℋA0ℎ
2 oveq2 ⊢A=ifA∈ℋA0ℎ→B⋅ℎA=B⋅ℎifA∈ℋA0ℎ
3 1 2 eqeq12d ⊢A=ifA∈ℋA0ℎ→T⁡A=B⋅ℎA↔T⁡ifA∈ℋA0ℎ=B⋅ℎifA∈ℋA0ℎ
4 neeq1 ⊢A=ifA∈ℋA0ℎ→A≠0ℎ↔ifA∈ℋA0ℎ≠0ℎ
5 3 4 anbi12d ⊢A=ifA∈ℋA0ℎ→T⁡A=B⋅ℎA∧A≠0ℎ↔T⁡ifA∈ℋA0ℎ=B⋅ℎifA∈ℋA0ℎ∧ifA∈ℋA0ℎ≠0ℎ
6 id ⊢A=ifA∈ℋA0ℎ→A=ifA∈ℋA0ℎ
7 6 1 oveq12d ⊢A=ifA∈ℋA0ℎ→A⋅ihT⁡A=ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ
8 1 6 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A⋅ihA=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ
9 7 8 eqeq12d ⊢A=ifA∈ℋA0ℎ→A⋅ihT⁡A=T⁡A⋅ihA↔ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ
10 9 bibi1d ⊢A=ifA∈ℋA0ℎ→A⋅ihT⁡A=T⁡A⋅ihA↔B∈ℝ↔ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ↔B∈ℝ
11 5 10 imbi12d ⊢A=ifA∈ℋA0ℎ→T⁡A=B⋅ℎA∧A≠0ℎ→A⋅ihT⁡A=T⁡A⋅ihA↔B∈ℝ↔T⁡ifA∈ℋA0ℎ=B⋅ℎifA∈ℋA0ℎ∧ifA∈ℋA0ℎ≠0ℎ→ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ↔B∈ℝ
12 oveq1 ⊢B=ifB∈ℂB0→B⋅ℎifA∈ℋA0ℎ=ifB∈ℂB0⋅ℎifA∈ℋA0ℎ
13 12 eqeq2d ⊢B=ifB∈ℂB0→T⁡ifA∈ℋA0ℎ=B⋅ℎifA∈ℋA0ℎ↔T⁡ifA∈ℋA0ℎ=ifB∈ℂB0⋅ℎifA∈ℋA0ℎ
14 13 anbi1d ⊢B=ifB∈ℂB0→T⁡ifA∈ℋA0ℎ=B⋅ℎifA∈ℋA0ℎ∧ifA∈ℋA0ℎ≠0ℎ↔T⁡ifA∈ℋA0ℎ=ifB∈ℂB0⋅ℎifA∈ℋA0ℎ∧ifA∈ℋA0ℎ≠0ℎ
15 eleq1 ⊢B=ifB∈ℂB0→B∈ℝ↔ifB∈ℂB0∈ℝ
16 15 bibi2d ⊢B=ifB∈ℂB0→ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ↔B∈ℝ↔ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ↔ifB∈ℂB0∈ℝ
17 14 16 imbi12d ⊢B=ifB∈ℂB0→T⁡ifA∈ℋA0ℎ=B⋅ℎifA∈ℋA0ℎ∧ifA∈ℋA0ℎ≠0ℎ→ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ↔B∈ℝ↔T⁡ifA∈ℋA0ℎ=ifB∈ℂB0⋅ℎifA∈ℋA0ℎ∧ifA∈ℋA0ℎ≠0ℎ→ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ↔ifB∈ℂB0∈ℝ
18 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
19 0cn ⊢0∈ℂ
20 19 elimel ⊢ifB∈ℂB0∈ℂ
21 18 20 eigrei ⊢T⁡ifA∈ℋA0ℎ=ifB∈ℂB0⋅ℎifA∈ℋA0ℎ∧ifA∈ℋA0ℎ≠0ℎ→ifA∈ℋA0ℎ⋅ihT⁡ifA∈ℋA0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifA∈ℋA0ℎ↔ifB∈ℂB0∈ℝ
22 11 17 21 dedth2h ⊢A∈ℋ∧B∈ℂ→T⁡A=B⋅ℎA∧A≠0ℎ→A⋅ihT⁡A=T⁡A⋅ihA↔B∈ℝ
23 22 imp ⊢A∈ℋ∧B∈ℂ∧T⁡A=B⋅ℎA∧A≠0ℎ→A⋅ihT⁡A=T⁡A⋅ihA↔B∈ℝ