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	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐴 ∈ ℋ )

Proof

Step	Hyp	Ref	Expression
1		eleigvec2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝐴 ∈ ( eigvec ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) ) )
2	1	biimpa	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) )
3	2	simp1d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐴 ∈ ℋ )