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