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 : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. CC )

Proof

Step Hyp Ref Expression
1 eigvalval 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) = ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) )
2 eleigveccl 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A e. ~H )
3 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ A e. ~H ) -> ( T ` A ) e. ~H )
4 hicl 
 |-  ( ( ( T ` A ) e. ~H /\ A e. ~H ) -> ( ( T ` A ) .ih A ) e. CC )
5 3 4 sylancom 
 |-  ( ( T : ~H --> ~H /\ A e. ~H ) -> ( ( T ` A ) .ih A ) e. CC )
6 2 5 syldan 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( T ` A ) .ih A ) e. CC )
7 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
8 7 recnd 
 |-  ( A e. ~H -> ( normh ` A ) e. CC )
9 2 8 syl 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( normh ` A ) e. CC )
10 9 sqcld 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( normh ` A ) ^ 2 ) e. CC )
11 eleigvec 
 |-  ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) ) )
12 11 biimpa 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
13 sqne0 
 |-  ( ( normh ` A ) e. CC -> ( ( ( normh ` A ) ^ 2 ) =/= 0 <-> ( normh ` A ) =/= 0 ) )
14 8 13 syl 
 |-  ( A e. ~H -> ( ( ( normh ` A ) ^ 2 ) =/= 0 <-> ( normh ` A ) =/= 0 ) )
15 normne0 
 |-  ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
16 14 15 bitr2d 
 |-  ( A e. ~H -> ( A =/= 0h <-> ( ( normh ` A ) ^ 2 ) =/= 0 ) )
17 16 biimpa 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( normh ` A ) ^ 2 ) =/= 0 )
18 17 3adant3 
 |-  ( ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) -> ( ( normh ` A ) ^ 2 ) =/= 0 )
19 12 18 syl 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( normh ` A ) ^ 2 ) =/= 0 )
20 6 10 19 divcld 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) e. CC )
21 1 20 eqeltrd 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. CC )