lsm02

Description: Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsm01.z	$⊢ \underset{˙}{0} = 0_{G}$
	lsm01.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
Assertion	lsm02	$⊢ X \in SubGrp (G) \to \{\underset{˙}{0}\} \underset{˙}{\oplus} X = X$

Step	Hyp	Ref	Expression
1		lsm01.z	$⊢ \underset{˙}{0} = 0_{G}$
2		lsm01.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		subgrcl	$⊢ X \in SubGrp (G) \to G \in Grp$
4	1	0subg	$⊢ G \in Grp \to \{\underset{˙}{0}\} \in SubGrp (G)$
5	3 4	syl	$⊢ X \in SubGrp (G) \to \{\underset{˙}{0}\} \in SubGrp (G)$
6		id	$⊢ X \in SubGrp (G) \to X \in SubGrp (G)$
7	1	subg0cl	$⊢ X \in SubGrp (G) \to \underset{˙}{0} \in X$
8	7	snssd	$⊢ X \in SubGrp (G) \to \{\underset{˙}{0}\} \subseteq X$
9	2	lsmss1	$⊢ (\{\underset{˙}{0}\} \in SubGrp (G) \land X \in SubGrp (G) \land \{\underset{˙}{0}\} \subseteq X) \to \{\underset{˙}{0}\} \underset{˙}{\oplus} X = X$
10	5 6 8 9	syl3anc	$⊢ X \in SubGrp (G) \to \{\underset{˙}{0}\} \underset{˙}{\oplus} X = X$

Metamath Proof Explorer