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