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 \in LMod \land X \in V) \to N (\{X\}) \in 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 \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
5	3	lsssubg	$⊢ (W \in LMod \land N (\{X\}) \in LSubSp (W)) \to N (\{X\}) \in SubGrp (W)$
6	4 5	syldan	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in SubGrp (W)$