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=\left\{x\in X|\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\right\}$$
	nmzsubg.2	$$⊢X={\mathrm{Base}}_G$$
	nmzsubg.3	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	isnsg4	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge N=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		elnmz.1	$$⊢N=\left\{x\in X|\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\right\}$$
2		nmzsubg.2	$$⊢X={\mathrm{Base}}_G$$
3		nmzsubg.3	$$⊢\underset{\dot{}}{+}={+}_G$$
4	2 3	isnsg	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\right)$$
5		eqcom	$$⊢N=X\leftrightarrow X=N$$
6	1	eqeq2i	$$⊢X=N\leftrightarrow X=\left\{x\in X|\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\right\}$$
7		rabid2	$$⊢X=\left\{x\in X|\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\right\}\leftrightarrow \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)$$
8	5 6 7	3bitri	$$⊢N=X\leftrightarrow \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)$$
9	8	anbi2i	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge N=X\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\right)$$
10	4 9	bitr4i	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge N=X\right)$$