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 ∈ X x + ˙ y ∈ S ↔ y + ˙ x ∈ S
nmzsubg.2 ⊢ X = Base G
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 ∈ X x + ˙ y ∈ S ↔ y + ˙ x ∈ S
2 nmzsubg.2 ⊢ X = Base G
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 ∈ N z + ˙ w ∈ S ↔ w + ˙ z ∈ S
18 4 subgbas ⊢ N ∈ SubGrp ⁡ G → N = Base H
19 9 18 syl ⊢ S ∈ SubGrp ⁡ G → N = Base H
20 19 raleqdv ⊢ S ∈ SubGrp ⁡ G → ∀ w ∈ N z + ˙ w ∈ S ↔ w + ˙ z ∈ S ↔ ∀ w ∈ Base H z + ˙ w ∈ S ↔ w + ˙ z ∈ S
21 19 20 raleqbidv ⊢ S ∈ SubGrp ⁡ G → ∀ z ∈ N ∀ w ∈ N z + ˙ w ∈ S ↔ w + ˙ z ∈ S ↔ ∀ z ∈ Base H ∀ w ∈ Base H z + ˙ w ∈ S ↔ w + ˙ z ∈ S
22 17 21 mpbii ⊢ S ∈ SubGrp ⁡ G → ∀ z ∈ Base H ∀ w ∈ Base H z + ˙ w ∈ S ↔ w + ˙ z ∈ S
23 eqid ⊢ Base H = Base H
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 ∈ Base H ∀ w ∈ Base H z + ˙ w ∈ S ↔ w + ˙ z ∈ S
29 12 22 28 sylanbrc ⊢ S ∈ SubGrp ⁡ G → S ∈ NrmSGrp ⁡ H