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

Metamath Proof Explorer

Theorem lsm01

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 lsm01 
|- ( X e. ( SubGrp ` G ) -> ( X .(+) { .0. } ) = 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 1 subg0cl 
 |-  ( X e. ( SubGrp ` G ) -> .0. e. X )
7 6 snssd 
 |-  ( X e. ( SubGrp ` G ) -> { .0. } C_ X )
8 2 lsmss2 
 |-  ( ( X e. ( SubGrp ` G ) /\ { .0. } e. ( SubGrp ` G ) /\ { .0. } C_ X ) -> ( X .(+) { .0. } ) = X )
9 5 7 8 mpd3an23 
 |-  ( X e. ( SubGrp ` G ) -> ( X .(+) { .0. } ) = X )