Theorem conjnsg

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

	Ref	Expression
Hypotheses	conjghm.x	|- X = ( Base ` G )
	conjghm.p	|- .+ = ( +g ` G )
	conjghm.m	|- .- = ( -g ` G )
	conjsubg.f	|- F = ( x e. S |-> ( ( A .+ x ) .- A ) )
Assertion	conjnsg	|- ( ( S e. ( NrmSGrp ` G ) /\ A e. X ) -> S = ran F )

Proof

Step	Hyp	Ref	Expression
1		conjghm.x	|- X = ( Base ` G )
2		conjghm.p	|- .+ = ( +g ` G )
3		conjghm.m	|- .- = ( -g ` G )
4		conjsubg.f	|- F = ( x e. S |-> ( ( A .+ x ) .- A ) )
5		nsgsubg	|- ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
6		eqid	|- { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) } = { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) }
7	6 1 2	isnsg4	|- ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) } = X ) )
8	7	simprbi	|- ( S e. ( NrmSGrp ` G ) -> { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) } = X )
9	8	eleq2d	|- ( S e. ( NrmSGrp ` G ) -> ( A e. { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) } <-> A e. X ) )
10	9	biimpar	|- ( ( S e. ( NrmSGrp ` G ) /\ A e. X ) -> A e. { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) } )
11	1 2 3 4 6	conjnmz	|- ( ( S e. ( SubGrp ` G ) /\ A e. { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) } ) -> S = ran F )
12	5 10 11	syl2an2r	|- ( ( S e. ( NrmSGrp ` G ) /\ A e. X ) -> S = ran F )