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	$⊢ \underset{˙}{+} = +_{G}$
	conjghm.m	$⊢ \underset{˙}{-} = -_{G}$
	conjsubg.f	$⊢ F = (x \in S ⟼ (A \underset{˙}{+} x) \underset{˙}{-} A)$
Assertion	conjnsg	$⊢ (S \in NrmSGrp (G) \land A \in X) \to S = ran F$

Step	Hyp	Ref	Expression
1		conjghm.x	$⊢ X = {Base}_{G}$
2		conjghm.p	$⊢ \underset{˙}{+} = +_{G}$
3		conjghm.m	$⊢ \underset{˙}{-} = -_{G}$
4		conjsubg.f	$⊢ F = (x \in S ⟼ (A \underset{˙}{+} x) \underset{˙}{-} A)$
5		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
6		eqid	$⊢ \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\} = \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\}$
7	6 1 2	isnsg4	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\} = X)$
8	7	simprbi	$⊢ S \in NrmSGrp (G) \to \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\} = X$
9	8	eleq2d	$⊢ S \in NrmSGrp (G) \to (A \in \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\} \leftrightarrow A \in X)$
10	9	biimpar	$⊢ (S \in NrmSGrp (G) \land A \in X) \to A \in \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\}$
11	1 2 3 4 6	conjnmz	$⊢ (S \in SubGrp (G) \land A \in \{y \in X \| \forall z \in X (y \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} y \in S)\}) \to S = ran F$
12	5 10 11	syl2an2r	$⊢ (S \in NrmSGrp (G) \land A \in X) \to S = ran F$

Metamath Proof Explorer