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 = ( Base ` W )
	lspsnsubg.n	|- N = ( LSpan ` W )
Assertion	lspsnsubg	|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )

Proof

Step	Hyp	Ref	Expression
1		lspsnsubg.v	|- V = ( Base ` W )
2		lspsnsubg.n	|- N = ( LSpan ` W )
3		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
4	1 3 2	lspsncl	|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
5	3	lsssubg	|- ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
6	4 5	syldan	|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )