This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )