Metamath Proof Explorer

Theorem eleigveccl

Description: Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	eleigveccl	\|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A e. ~H )

Step	Hyp	Ref	Expression
1		eleigvec2	\|- ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) ) )
2	1	biimpa	\|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) )
3	2	simp1d	\|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A e. ~H )

Step

Hyp

Ref

Expression

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

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

 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A e. ~H )