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 𝐹 )