Metamath Proof Explorer

Theorem eleigvec2

Description: Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eleigvec2 
|- ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) ) )

Proof

Step Hyp Ref Expression
1 eleigvec 
 |-  ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) ) )
2 elspansn 
 |-  ( A e. ~H -> ( ( T ` A ) e. ( span ` { A } ) <-> E. x e. CC ( T ` A ) = ( x .h A ) ) )
3 2 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( T ` A ) e. ( span ` { A } ) <-> E. x e. CC ( T ` A ) = ( x .h A ) ) )
4 3 pm5.32i 
 |-  ( ( ( A e. ~H /\ A =/= 0h ) /\ ( T ` A ) e. ( span ` { A } ) ) <-> ( ( A e. ~H /\ A =/= 0h ) /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
5 df-3an 
 |-  ( ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) <-> ( ( A e. ~H /\ A =/= 0h ) /\ ( T ` A ) e. ( span ` { A } ) ) )
6 df-3an 
 |-  ( ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) <-> ( ( A e. ~H /\ A =/= 0h ) /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
7 4 5 6 3bitr4i 
 |-  ( ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )
8 1 7 bitr4di 
 |-  ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) ) )