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 ‘ 𝐻 ) )