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

Metamath Proof Explorer

Theorem subg0

Description: A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses subg0.h 
|- H = ( G |`s S )
subg0.i 
|- .0. = ( 0g ` G )
Assertion subg0 
|- ( S e. ( SubGrp ` G ) -> .0. = ( 0g ` H ) )

Proof

Step Hyp Ref Expression
1 subg0.h 
 |-  H = ( G |`s S )
2 subg0.i 
 |-  .0. = ( 0g ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 1 3 ressplusg 
 |-  ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
5 4 oveqd 
 |-  ( S e. ( SubGrp ` G ) -> ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( ( 0g ` H ) ( +g ` H ) ( 0g ` H ) ) )
6 1 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> H e. Grp )
7 eqid 
 |-  ( Base ` H ) = ( Base ` H )
8 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
9 7 8 grpidcl 
 |-  ( H e. Grp -> ( 0g ` H ) e. ( Base ` H ) )
10 6 9 syl 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` H ) e. ( Base ` H ) )
11 eqid 
 |-  ( +g ` H ) = ( +g ` H )
12 7 11 8 grplid 
 |-  ( ( H e. Grp /\ ( 0g ` H ) e. ( Base ` H ) ) -> ( ( 0g ` H ) ( +g ` H ) ( 0g ` H ) ) = ( 0g ` H ) )
13 6 10 12 syl2anc 
 |-  ( S e. ( SubGrp ` G ) -> ( ( 0g ` H ) ( +g ` H ) ( 0g ` H ) ) = ( 0g ` H ) )
14 5 13 eqtrd 
 |-  ( S e. ( SubGrp ` G ) -> ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( 0g ` H ) )
15 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
16 eqid 
 |-  ( Base ` G ) = ( Base ` G )
17 16 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
18 1 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
19 10 18 eleqtrrd 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` H ) e. S )
20 17 19 sseldd 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` H ) e. ( Base ` G ) )
21 16 3 2 grpid 
 |-  ( ( G e. Grp /\ ( 0g ` H ) e. ( Base ` G ) ) -> ( ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( 0g ` H ) <-> .0. = ( 0g ` H ) ) )
22 15 20 21 syl2anc 
 |-  ( S e. ( SubGrp ` G ) -> ( ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( 0g ` H ) <-> .0. = ( 0g ` H ) ) )
23 14 22 mpbid 
 |-  ( S e. ( SubGrp ` G ) -> .0. = ( 0g ` H ) )