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