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 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
nmznsg.4 ⊢ 𝐻 = ( 𝐺 ↾s 𝑁 )
Assertion nmznsg ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( NrmSGrp ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
2 nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
4 nmznsg.4 ⊢ 𝐻 = ( 𝐺 ↾s 𝑁 )
5 id ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
6 1 2 3 ssnmz ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑁 )
7 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
8 1 2 3 nmzsubg ⊢ ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
9 7 8 syl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
10 4 subsubg ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑁 ) ) )
11 9 10 syl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑁 ) ) )
12 5 6 11 mpbir2and ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐻 ) )
13 1 ssrab3 ⊢ 𝑁 ⊆ 𝑋
14 13 sseli ⊢ ( 𝑤 ∈ 𝑁 → 𝑤 ∈ 𝑋 )
15 1 nmzbi ⊢ ( ( 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
16 14 15 sylan2 ⊢ ( ( 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) → ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
17 16 rgen2 ⊢ ∀ 𝑧 ∈ 𝑁 ∀ 𝑤 ∈ 𝑁 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 )
18 4 subgbas ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 = ( Base ‘ 𝐻 ) )
19 9 18 syl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 = ( Base ‘ 𝐻 ) )
20 19 raleqdv ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑤 ∈ 𝑁 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) )
21 19 20 raleqbidv ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑧 ∈ 𝑁 ∀ 𝑤 ∈ 𝑁 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) )
22 17 21 mpbii ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
23 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
24 2 fvexi ⊢ 𝑋 ∈ V
25 24 13 ssexi ⊢ 𝑁 ∈ V
26 4 3 ressplusg ⊢ ( 𝑁 ∈ V → + = ( +g ‘ 𝐻 ) )
27 25 26 ax-mp ⊢ + = ( +g ‘ 𝐻 )
28 23 27 isnsg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐻 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) )
29 12 22 28 sylanbrc ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( NrmSGrp ‘ 𝐻 ) )