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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsnsubg.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		lspsnsubg.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsnsubg.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
4	1 3 2	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
5	3	lsssubg	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
6	4 5	syldan	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )