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 ` G )
lsm01.p
|- .(+) = ( LSSum ` G )
Assertion lsm02
|- ( X e. ( SubGrp ` G ) -> ( { .0. } .(+) X ) = X )

Proof

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 )