Metamath Proof Explorer

Theorem nmznsg

Description: Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses elnmz.1 ⊢N=x∈X|∀y∈Xx+˙y∈S↔y+˙x∈S
nmzsubg.2 ⊢X=BaseG
nmzsubg.3 ⊢+˙=+G
nmznsg.4 ⊢H=G↾𝑠N
Assertion nmznsg ⊢S∈SubGrp⁡G→S∈NrmSGrp⁡H

Proof

Step Hyp Ref Expression
1 elnmz.1 ⊢N=x∈X|∀y∈Xx+˙y∈S↔y+˙x∈S
2 nmzsubg.2 ⊢X=BaseG
3 nmzsubg.3 ⊢+˙=+G
4 nmznsg.4 ⊢H=G↾𝑠N
5 id ⊢S∈SubGrp⁡G→S∈SubGrp⁡G
6 1 2 3 ssnmz ⊢S∈SubGrp⁡G→S⊆N
7 subgrcl ⊢S∈SubGrp⁡G→G∈Grp
8 1 2 3 nmzsubg ⊢G∈Grp→N∈SubGrp⁡G
9 7 8 syl ⊢S∈SubGrp⁡G→N∈SubGrp⁡G
10 4 subsubg ⊢N∈SubGrp⁡G→S∈SubGrp⁡H↔S∈SubGrp⁡G∧S⊆N
11 9 10 syl ⊢S∈SubGrp⁡G→S∈SubGrp⁡H↔S∈SubGrp⁡G∧S⊆N
12 5 6 11 mpbir2and ⊢S∈SubGrp⁡G→S∈SubGrp⁡H
13 1 ssrab3 ⊢N⊆X
14 13 sseli ⊢w∈N→w∈X
15 1 nmzbi ⊢z∈N∧w∈X→z+˙w∈S↔w+˙z∈S
16 14 15 sylan2 ⊢z∈N∧w∈N→z+˙w∈S↔w+˙z∈S
17 16 rgen2 ⊢∀z∈N∀w∈Nz+˙w∈S↔w+˙z∈S
18 4 subgbas ⊢N∈SubGrp⁡G→N=BaseH
19 9 18 syl ⊢S∈SubGrp⁡G→N=BaseH
20 19 raleqdv ⊢S∈SubGrp⁡G→∀w∈Nz+˙w∈S↔w+˙z∈S↔∀w∈BaseHz+˙w∈S↔w+˙z∈S
21 19 20 raleqbidv ⊢S∈SubGrp⁡G→∀z∈N∀w∈Nz+˙w∈S↔w+˙z∈S↔∀z∈BaseH∀w∈BaseHz+˙w∈S↔w+˙z∈S
22 17 21 mpbii ⊢S∈SubGrp⁡G→∀z∈BaseH∀w∈BaseHz+˙w∈S↔w+˙z∈S
23 eqid ⊢BaseH=BaseH
24 2 fvexi ⊢X∈V
25 24 13 ssexi ⊢N∈V
26 4 3 ressplusg ⊢N∈V→+˙=+H
27 25 26 ax-mp ⊢+˙=+H
28 23 27 isnsg ⊢S∈NrmSGrp⁡H↔S∈SubGrp⁡H∧∀z∈BaseH∀w∈BaseHz+˙w∈S↔w+˙z∈S
29 12 22 28 sylanbrc ⊢S∈SubGrp⁡G→S∈NrmSGrp⁡H