Metamath Proof Explorer

Theorem eigvec1

Description: Property of an eigenvector. (Contributed by NM, 12-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigvec1 
|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) )

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 1 oveq1d 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( ( eigval ` T ) ` A ) .h A ) = ( ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) )
3 eleigvec2 
 |-  ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) ) )
4 3 biimpa 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) )
5 normcan 
 |-  ( ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) -> ( ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) = ( T ` A ) )
6 4 5 syl 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) = ( T ` A ) )
7 2 6 eqtr2d 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) )
8 4 simp2d 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A =/= 0h )
9 7 8 jca 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) )