This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isnsg4

Description: A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
Assertion isnsg4 ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
2 nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
4 2 3 isnsg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
5 eqcom ⊢ ( 𝑁 = 𝑋 ↔ 𝑋 = 𝑁 )
6 1 eqeq2i ⊢ ( 𝑋 = 𝑁 ↔ 𝑋 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) } )
7 rabid2 ⊢ ( 𝑋 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) } ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
8 5 6 7 3bitri ⊢ ( 𝑁 = 𝑋 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
9 8 anbi2i ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 = 𝑋 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
10 4 9 bitr4i ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 = 𝑋 ) )