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 AspanAS

Proof

Step Hyp Ref Expression
1 spansnch AspanAC
2 chsh spanACspanAS
3 1 2 syl AspanAS