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