Step |
Hyp |
Ref |
Expression |
1 |
|
lsm01.z |
|- .0. = ( 0g ` G ) |
2 |
|
lsm01.p |
|- .(+) = ( LSSum ` G ) |
3 |
|
subgrcl |
|- ( X e. ( SubGrp ` G ) -> G e. Grp ) |
4 |
1
|
0subg |
|- ( G e. Grp -> { .0. } e. ( SubGrp ` G ) ) |
5 |
3 4
|
syl |
|- ( X e. ( SubGrp ` G ) -> { .0. } e. ( SubGrp ` G ) ) |
6 |
|
id |
|- ( X e. ( SubGrp ` G ) -> X e. ( SubGrp ` G ) ) |
7 |
1
|
subg0cl |
|- ( X e. ( SubGrp ` G ) -> .0. e. X ) |
8 |
7
|
snssd |
|- ( X e. ( SubGrp ` G ) -> { .0. } C_ X ) |
9 |
2
|
lsmss1 |
|- ( ( { .0. } e. ( SubGrp ` G ) /\ X e. ( SubGrp ` G ) /\ { .0. } C_ X ) -> ( { .0. } .(+) X ) = X ) |
10 |
5 6 8 9
|
syl3anc |
|- ( X e. ( SubGrp ` G ) -> ( { .0. } .(+) X ) = X ) |