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

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

Metamath Proof Explorer