Metamath Proof Explorer

Theorem lspsncl

Description: The span of a singleton is a subspace (frequently used special case of lspcl ). (Contributed by NM, 17-Jul-2014)

Ref Expression
Hypotheses lspval.v V = Base W
lspval.s S = LSubSp W
lspval.n N = LSpan W
Assertion lspsncl W LMod X V N X S


Step Hyp Ref Expression
1 lspval.v V = Base W
2 lspval.s S = LSubSp W
3 lspval.n N = LSpan W
4 snssi X V X V
5 1 2 3 lspcl W LMod X V N X S
6 4 5 sylan2 W LMod X V N X S