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

Metamath Proof Explorer

Theorem conjnsg

Description: A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses conjghm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
conjghm.p ⊢ + = ( +g ‘ 𝐺 )
conjghm.m ⊢ − = ( -g ‘ 𝐺 )
conjsubg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
Assertion conjnsg ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 = ran 𝐹 )

Proof

Step Hyp Ref Expression
1 conjghm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 conjghm.p ⊢ + = ( +g ‘ 𝐺 )
3 conjghm.m ⊢ − = ( -g ‘ 𝐺 )
4 conjsubg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
5 nsgsubg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
6 eqid ⊢ { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) } = { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) }
7 6 1 2 isnsg4 ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) } = 𝑋 ) )
8 7 simprbi ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) } = 𝑋 )
9 8 eleq2d ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) } ↔ 𝐴 ∈ 𝑋 ) )
10 9 biimpar ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) } )
11 1 2 3 4 6 conjnmz ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) } ) → 𝑆 = ran 𝐹 )
12 5 10 11 syl2an2r ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 = ran 𝐹 )