isnsg3

Description: A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	isnsg3.1	$⊢ X = {Base}_{G}$
	isnsg3.2	$⊢ \underset{˙}{+} = +_{G}$
	isnsg3.3	$⊢ \underset{˙}{-} = -_{G}$
Assertion	isnsg3	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S)$

Proof

Step	Hyp	Ref	Expression
1		isnsg3.1	$⊢ X = {Base}_{G}$
2		isnsg3.2	$⊢ \underset{˙}{+} = +_{G}$
3		isnsg3.3	$⊢ \underset{˙}{-} = -_{G}$
4		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
5	1 2 3	nsgconj	$⊢ (S \in NrmSGrp (G) \land x \in X \land y \in S) \to (x \underset{˙}{+} y) \underset{˙}{-} x \in S$
6	5	3expb	$⊢ (S \in NrmSGrp (G) \land (x \in X \land y \in S)) \to (x \underset{˙}{+} y) \underset{˙}{-} x \in S$
7	6	ralrimivva	$⊢ S \in NrmSGrp (G) \to \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S$
8	4 7	jca	$⊢ S \in NrmSGrp (G) \to (S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S)$
9		simpl	$⊢ (S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \to S \in SubGrp (G)$
10		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
11	10	ad2antrr	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to G \in Grp$
12		simprll	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to z \in X$
13		eqid	$⊢ 0_{G} = 0_{G}$
14		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
15	1 2 13 14	grplinv	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
16	11 12 15	syl2anc	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
17	16	oveq1d	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to ({inv}_{g} (G) (z) \underset{˙}{+} z) \underset{˙}{+} w = 0_{G} \underset{˙}{+} w$
18	1 14	grpinvcl	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \in X$
19	11 12 18	syl2anc	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to {inv}_{g} (G) (z) \in X$
20		simprlr	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to w \in X$
21	1 2	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (z) \in X \land z \in X \land w \in X)) \to ({inv}_{g} (G) (z) \underset{˙}{+} z) \underset{˙}{+} w = {inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)$
22	11 19 12 20 21	syl13anc	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to ({inv}_{g} (G) (z) \underset{˙}{+} z) \underset{˙}{+} w = {inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)$
23	1 2 13	grplid	$⊢ (G \in Grp \land w \in X) \to 0_{G} \underset{˙}{+} w = w$
24	11 20 23	syl2anc	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to 0_{G} \underset{˙}{+} w = w$
25	17 22 24	3eqtr3d	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to {inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w) = w$
26	25	oveq1d	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to ({inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)) \underset{˙}{-} {inv}_{g} (G) (z) = w \underset{˙}{-} {inv}_{g} (G) (z)$
27	1 2 3 14 11 20 12	grpsubinv	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to w \underset{˙}{-} {inv}_{g} (G) (z) = w \underset{˙}{+} z$
28	26 27	eqtrd	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to ({inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)) \underset{˙}{-} {inv}_{g} (G) (z) = w \underset{˙}{+} z$
29		simprr	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to z \underset{˙}{+} w \in S$
30		simplr	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S$
31		oveq1	$⊢ x = {inv}_{g} (G) (z) \to x \underset{˙}{+} y = {inv}_{g} (G) (z) \underset{˙}{+} y$
32		id	$⊢ x = {inv}_{g} (G) (z) \to x = {inv}_{g} (G) (z)$
33	31 32	oveq12d	$⊢ x = {inv}_{g} (G) (z) \to (x \underset{˙}{+} y) \underset{˙}{-} x = ({inv}_{g} (G) (z) \underset{˙}{+} y) \underset{˙}{-} {inv}_{g} (G) (z)$
34	33	eleq1d	$⊢ x = {inv}_{g} (G) (z) \to ((x \underset{˙}{+} y) \underset{˙}{-} x \in S \leftrightarrow ({inv}_{g} (G) (z) \underset{˙}{+} y) \underset{˙}{-} {inv}_{g} (G) (z) \in S)$
35		oveq2	$⊢ y = z \underset{˙}{+} w \to {inv}_{g} (G) (z) \underset{˙}{+} y = {inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)$
36	35	oveq1d	$⊢ y = z \underset{˙}{+} w \to ({inv}_{g} (G) (z) \underset{˙}{+} y) \underset{˙}{-} {inv}_{g} (G) (z) = ({inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)) \underset{˙}{-} {inv}_{g} (G) (z)$
37	36	eleq1d	$⊢ y = z \underset{˙}{+} w \to (({inv}_{g} (G) (z) \underset{˙}{+} y) \underset{˙}{-} {inv}_{g} (G) (z) \in S \leftrightarrow ({inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)) \underset{˙}{-} {inv}_{g} (G) (z) \in S)$
38	34 37	rspc2va	$⊢ (({inv}_{g} (G) (z) \in X \land z \underset{˙}{+} w \in S) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \to ({inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)) \underset{˙}{-} {inv}_{g} (G) (z) \in S$
39	19 29 30 38	syl21anc	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to ({inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w)) \underset{˙}{-} {inv}_{g} (G) (z) \in S$
40	28 39	eqeltrrd	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land ((z \in X \land w \in X) \land z \underset{˙}{+} w \in S)) \to w \underset{˙}{+} z \in S$
41	40	expr	$⊢ ((S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \land (z \in X \land w \in X)) \to (z \underset{˙}{+} w \in S \to w \underset{˙}{+} z \in S)$
42	41	ralrimivva	$⊢ (S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \to \forall z \in X \forall w \in X (z \underset{˙}{+} w \in S \to w \underset{˙}{+} z \in S)$
43	1 2	isnsg2	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall z \in X \forall w \in X (z \underset{˙}{+} w \in S \to w \underset{˙}{+} z \in S))$
44	9 42 43	sylanbrc	$⊢ (S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S) \to S \in NrmSGrp (G)$
45	8 44	impbii	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall x \in X \forall y \in S (x \underset{˙}{+} y) \underset{˙}{-} x \in S)$

Metamath Proof Explorer

Theorem isnsg3

Proof