Metamath Proof Explorer


Theorem lsm01

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 0˙=0G
lsm01.p ˙=LSSumG
Assertion lsm01 XSubGrpGX˙0˙=X

Proof

Step Hyp Ref Expression
1 lsm01.z 0˙=0G
2 lsm01.p ˙=LSSumG
3 subgrcl XSubGrpGGGrp
4 1 0subg GGrp0˙SubGrpG
5 3 4 syl XSubGrpG0˙SubGrpG
6 1 subg0cl XSubGrpG0˙X
7 6 snssd XSubGrpG0˙X
8 2 lsmss2 XSubGrpG0˙SubGrpG0˙XX˙0˙=X
9 5 7 8 mpd3an23 XSubGrpGX˙0˙=X