Metamath Proof Explorer

Theorem eigvalcl

Description: An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigvalcl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A ∈ ℂ

Proof

Step Hyp Ref Expression
1 eigvalval ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A = T ⁡ A ⋅ ih A norm ℎ ⁡ A 2
2 eleigveccl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → A ∈ ℋ
3 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → T ⁡ A ∈ ℋ
4 hicl ⊢ T ⁡ A ∈ ℋ ∧ A ∈ ℋ → T ⁡ A ⋅ ih A ∈ ℂ
5 3 4 sylancom ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → T ⁡ A ⋅ ih A ∈ ℂ
6 2 5 syldan ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → T ⁡ A ⋅ ih A ∈ ℂ
7 normcl ⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℝ
8 7 recnd ⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℂ
9 2 8 syl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → norm ℎ ⁡ A ∈ ℂ
10 9 sqcld ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → norm ℎ ⁡ A 2 ∈ ℂ
11 eleigvec ⊢ T : ℋ ⟶ ℋ → A ∈ eigvec ⁡ T ↔ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
12 11 biimpa ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A
13 sqne0 ⊢ norm ℎ ⁡ A ∈ ℂ → norm ℎ ⁡ A 2 ≠ 0 ↔ norm ℎ ⁡ A ≠ 0
14 8 13 syl ⊢ A ∈ ℋ → norm ℎ ⁡ A 2 ≠ 0 ↔ norm ℎ ⁡ A ≠ 0
15 normne0 ⊢ A ∈ ℋ → norm ℎ ⁡ A ≠ 0 ↔ A ≠ 0 ℎ
16 14 15 bitr2d ⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ norm ℎ ⁡ A 2 ≠ 0
17 16 biimpa ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A 2 ≠ 0
18 17 3adant3 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ ∃ x ∈ ℂ T ⁡ A = x ⋅ ℎ A → norm ℎ ⁡ A 2 ≠ 0
19 12 18 syl ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → norm ℎ ⁡ A 2 ≠ 0
20 6 10 19 divcld ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → T ⁡ A ⋅ ih A norm ℎ ⁡ A 2 ∈ ℂ
21 1 20 eqeltrd ⊢ T : ℋ ⟶ ℋ ∧ A ∈ eigvec ⁡ T → eigval ⁡ T ⁡ A ∈ ℂ