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	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	lsm01	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑋 ⊕ { 0 } ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		lsm01.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		lsm01.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
3		subgrcl	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
4	1	0subg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
5	3 4	syl	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
6	1	subg0cl	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑋 )
7	6	snssd	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → { 0 } ⊆ 𝑋 )
8	2	lsmss2	⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ⊆ 𝑋 ) → ( 𝑋 ⊕ { 0 } ) = 𝑋 )
9	5 7 8	mpd3an23	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑋 ⊕ { 0 } ) = 𝑋 )