Metamath Proof Explorer


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 } 𝑋 ) = 𝑋 )