# 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 ) ) )`
` |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( T ` A ) e. ( span ` { A } ) <-> E. x e. CC ( T ` A ) = ( x .h A ) ) )`
` |-  ( ( ( A e. ~H /\ A =/= 0h ) /\ ( T ` A ) e. ( span ` { A } ) ) <-> ( ( A e. ~H /\ A =/= 0h ) /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )`
` |-  ( ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) <-> ( ( A e. ~H /\ A =/= 0h ) /\ ( T ` A ) e. ( span ` { A } ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) )`
` |-  ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) ) )`