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
|- A e. ~H
Assertion spansnchi
|- ( span ` { A } ) e. CH

Proof

Step Hyp Ref Expression
1 spansnch.1
 |-  A e. ~H
2 spansnch
 |-  ( A e. ~H -> ( span ` { A } ) e. CH )
3 1 2 ax-mp
 |-  ( span ` { A } ) e. CH