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	⊢ 0 = ( 0g ‘ 𝐺 )
	lsm01.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	lsm02	⊢ ( 𝑋 ∈ ( 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		id	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → 𝑋 ∈ ( SubGrp ‘ 𝐺 ) )
7	1	subg0cl	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑋 )
8	7	snssd	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → { 0 } ⊆ 𝑋 )
9	2	lsmss1	⊢ ( ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ⊆ 𝑋 ) → ( { 0 } ⊕ 𝑋 ) = 𝑋 )
10	5 6 8 9	syl3anc	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → ( { 0 } ⊕ 𝑋 ) = 𝑋 )