This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem spansnchi

Description: The span of a singleton in Hilbert space is a closed subspace. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis spansnch.1 ⊢ 𝐴 ∈ ℋ
Assertion spansnchi ( span ‘ { 𝐴 } ) ∈ Cℋ

Proof

Step Hyp Ref Expression
1 spansnch.1 ⊢ 𝐴 ∈ ℋ
2 spansnch ⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ Cℋ )
3 1 2 ax-mp ⊢ ( span ‘ { 𝐴 } ) ∈ Cℋ