Theorem lspsnsubg

Description: The span of a singleton is an additive subgroup (frequently used special case of lspcl ). (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	lspsnsubg.v	$$⊢V={\mathrm{Base}}_W$$
	lspsnsubg.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	lspsnsubg	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspsnsubg.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsnsubg.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
4	1 3 2	lspsncl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
5	3	lsssubg	$$⊢\left(W\in \mathrm{LMod}\wedge N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(W\right)\right)\to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
6	4 5	syldan	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$