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
subg0.i 0˙=0G
Assertion subg0 SSubGrpG0˙=0H

Proof

Step Hyp Ref Expression
1 subg0.h H=G𝑠S
2 subg0.i 0˙=0G
3 eqid +G=+G
4 1 3 ressplusg SSubGrpG+G=+H
5 4 oveqd SSubGrpG0H+G0H=0H+H0H
6 1 subggrp SSubGrpGHGrp
7 eqid BaseH=BaseH
8 eqid 0H=0H
9 7 8 grpidcl HGrp0HBaseH
10 6 9 syl SSubGrpG0HBaseH
11 eqid +H=+H
12 7 11 8 grplid HGrp0HBaseH0H+H0H=0H
13 6 10 12 syl2anc SSubGrpG0H+H0H=0H
14 5 13 eqtrd SSubGrpG0H+G0H=0H
15 subgrcl SSubGrpGGGrp
16 eqid BaseG=BaseG
17 16 subgss SSubGrpGSBaseG
18 1 subgbas SSubGrpGS=BaseH
19 10 18 eleqtrrd SSubGrpG0HS
20 17 19 sseldd SSubGrpG0HBaseG
21 16 3 2 grpid GGrp0HBaseG0H+G0H=0H0˙=0H
22 15 20 21 syl2anc SSubGrpG0H+G0H=0H0˙=0H
23 14 22 mpbid SSubGrpG0˙=0H