Theorem 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{\dot{}}{0}=0_G$$
	lsm01.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
Assertion	lsm02	$$⊢X\in \mathrm{SubGrp}\left(G\right)\to \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }X=X$$

Proof

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