Metamath Proof Explorer


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 ) )