Metamath Proof Explorer


Theorem nsgid

Description: The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis nsgid.z B = Base G
Assertion nsgid G Grp B NrmSGrp G

Proof

Step Hyp Ref Expression
1 nsgid.z B = Base G
2 1 subgid G Grp B SubGrp G
3 simp1 G Grp x B y B G Grp
4 eqid + G = + G
5 1 4 grpcl G Grp x B y B x + G y B
6 simp2 G Grp x B y B x B
7 eqid - G = - G
8 1 7 grpsubcl G Grp x + G y B x B x + G y - G x B
9 3 5 6 8 syl3anc G Grp x B y B x + G y - G x B
10 9 3expb G Grp x B y B x + G y - G x B
11 10 ralrimivva G Grp x B y B x + G y - G x B
12 1 4 7 isnsg3 B NrmSGrp G B SubGrp G x B y B x + G y - G x B
13 2 11 12 sylanbrc G Grp B NrmSGrp G