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={\mathrm{Base}}_W$$
	lspval.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lspval.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	lspsncl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		lspval.v	$$⊢V={\mathrm{Base}}_W$$
2		lspval.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lspval.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		snssi	$$⊢X\in V\to \left\{X\right\}\subseteq V$$
5	1 2 3	lspcl	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{X\right\}\subseteq V\right)\to N\left(\left\{X\right\}\right)\in S$$
6	4 5	sylan2	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in S$$