Metamath Proof Explorer

Theorem spansnsh

Description: The span of a Hilbert space singleton is a subspace. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnsh 
|- ( A e. ~H -> ( span ` { A } ) e. SH )

Proof

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