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 
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
nmzsubg.2 
|- X = ( Base ` G )
nmzsubg.3 
|- .+ = ( +g ` G )
Assertion isnsg4 
|- ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ N = X ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
2 nmzsubg.2 
 |-  X = ( Base ` G )
3 nmzsubg.3 
 |-  .+ = ( +g ` G )
4 2 3 isnsg 
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )
5 eqcom 
 |-  ( N = X <-> X = N )
6 1 eqeq2i 
 |-  ( X = N <-> X = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) } )
7 rabid2 
 |-  ( X = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) } <-> A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) )
8 5 6 7 3bitri 
 |-  ( N = X <-> A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) )
9 8 anbi2i 
 |-  ( ( S e. ( SubGrp ` G ) /\ N = X ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )
10 4 9 bitr4i 
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ N = X ) )