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	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathrm{eigvec}\left(T\right)\right)\to A\in \mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		eleigvec2	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(A\in \mathrm{eigvec}\left(T\right)\leftrightarrow \left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\wedge T\left(A\right)\in \mathrm{span}\left(\left\{A\right\}\right)\right)\right)$$
2	1	biimpa	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathrm{eigvec}\left(T\right)\right)\to \left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\wedge T\left(A\right)\in \mathrm{span}\left(\left\{A\right\}\right)\right)$$
3	2	simp1d	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathrm{eigvec}\left(T\right)\right)\to A\in \mathscr{H}$$