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	$$⊢\underset{\dot{}}{0}=0_G$$
	lsm01.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
Assertion	lsm01	$$⊢X\in \mathrm{SubGrp}\left(G\right)\to X\underset{\dot{}}{\oplus }\left\{\underset{\dot{}}{0}\right\}=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	1	subg0cl	$$⊢X\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in X$$
7	6	snssd	$$⊢X\in \mathrm{SubGrp}\left(G\right)\to \left\{\underset{\dot{}}{0}\right\}\subseteq X$$
8	2	lsmss2	$$⊢\left(X\in \mathrm{SubGrp}\left(G\right)\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)\wedge \left\{\underset{\dot{}}{0}\right\}\subseteq X\right)\to X\underset{\dot{}}{\oplus }\left\{\underset{\dot{}}{0}\right\}=X$$
9	5 7 8	mpd3an23	$$⊢X\in \mathrm{SubGrp}\left(G\right)\to X\underset{\dot{}}{\oplus }\left\{\underset{\dot{}}{0}\right\}=X$$