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⋅ihAnormℎ⁡A2
2 eleigveccl ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→A∈ℋ
3 ffvelcdm ⊢T:ℋ⟶ℋ∧A∈ℋ→T⁡A∈ℋ
4 hicl ⊢T⁡A∈ℋ∧A∈ℋ→T⁡A⋅ihA∈ℂ
5 3 4 sylancom ⊢T:ℋ⟶ℋ∧A∈ℋ→T⁡A⋅ihA∈ℂ
6 2 5 syldan ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→T⁡A⋅ihA∈ℂ
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ℎ⁡A2∈ℂ
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ℎ⁡A2≠0↔normℎ⁡A≠0
14 8 13 syl ⊢A∈ℋ→normℎ⁡A2≠0↔normℎ⁡A≠0
15 normne0 ⊢A∈ℋ→normℎ⁡A≠0↔A≠0ℎ
16 14 15 bitr2d ⊢A∈ℋ→A≠0ℎ↔normℎ⁡A2≠0
17 16 biimpa ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A2≠0
18 17 3adant3 ⊢A∈ℋ∧A≠0ℎ∧∃x∈ℂT⁡A=x⋅ℎA→normℎ⁡A2≠0
19 12 18 syl ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→normℎ⁡A2≠0
20 6 10 19 divcld ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→T⁡A⋅ihAnormℎ⁡A2∈ℂ
21 1 20 eqeltrd ⊢T:ℋ⟶ℋ∧A∈eigvec⁡T→eigval⁡T⁡A∈ℂ