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=BaseG
Assertion nsgid ⊢G∈Grp→B∈NrmSGrp⁡G

Proof

Step Hyp Ref Expression
1 nsgid.z ⊢B=BaseG
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+Gy∈B
6 simp2 ⊢G∈Grp∧x∈B∧y∈B→x∈B
7 eqid ⊢-G=-G
8 1 7 grpsubcl ⊢G∈Grp∧x+Gy∈B∧x∈B→x+Gy-Gx∈B
9 3 5 6 8 syl3anc ⊢G∈Grp∧x∈B∧y∈B→x+Gy-Gx∈B
10 9 3expb ⊢G∈Grp∧x∈B∧y∈B→x+Gy-Gx∈B
11 10 ralrimivva ⊢G∈Grp→∀x∈B∀y∈Bx+Gy-Gx∈B
12 1 4 7 isnsg3 ⊢B∈NrmSGrp⁡G↔B∈SubGrp⁡G∧∀x∈B∀y∈Bx+Gy-Gx∈B
13 2 11 12 sylanbrc ⊢G∈Grp→B∈NrmSGrp⁡G