ssnmz

Description: A subgroup is a subset of its normalizer. (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	ssnmz	$⊢ S \in SubGrp (G) \to S \subseteq N$

Proof

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	subgss	$⊢ S \in SubGrp (G) \to S \subseteq X$
5	4	sselda	$⊢ (S \in SubGrp (G) \land z \in S) \to z \in X$
6		simpll	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to S \in SubGrp (G)$
7		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
8	6 7	syl	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to G \in Grp$
9	6 4	syl	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to S \subseteq X$
10		simplrl	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to z \in S$
11	9 10	sseldd	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to z \in X$
12		eqid	$⊢ 0_{G} = 0_{G}$
13		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
14	2 3 12 13	grplinv	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
15	8 11 14	syl2anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
16	15	oveq1d	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to ({inv}_{g} (G) (z) \underset{˙}{+} z) \underset{˙}{+} w = 0_{G} \underset{˙}{+} w$
17	13	subginvcl	$⊢ (S \in SubGrp (G) \land z \in S) \to {inv}_{g} (G) (z) \in S$
18	6 10 17	syl2anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to {inv}_{g} (G) (z) \in S$
19	9 18	sseldd	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to {inv}_{g} (G) (z) \in X$
20		simplrr	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to w \in X$
21	2 3	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	8 19 11 20 21	syl13anc	$⊢ ((S \in SubGrp (G) \land (z \in S \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	2 3 12	grplid	$⊢ (G \in Grp \land w \in X) \to 0_{G} \underset{˙}{+} w = w$
24	8 20 23	syl2anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to 0_{G} \underset{˙}{+} w = w$
25	16 22 24	3eqtr3d	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to {inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w) = w$
26		simpr	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to z \underset{˙}{+} w \in S$
27	3	subgcl	$⊢ (S \in SubGrp (G) \land {inv}_{g} (G) (z) \in S \land z \underset{˙}{+} w \in S) \to {inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w) \in S$
28	6 18 26 27	syl3anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to {inv}_{g} (G) (z) \underset{˙}{+} (z \underset{˙}{+} w) \in S$
29	25 28	eqeltrrd	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to w \in S$
30	3	subgcl	$⊢ (S \in SubGrp (G) \land w \in S \land z \in S) \to w \underset{˙}{+} z \in S$
31	6 29 10 30	syl3anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land z \underset{˙}{+} w \in S) \to w \underset{˙}{+} z \in S$
32		simpll	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to S \in SubGrp (G)$
33		simplrl	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to z \in S$
34	32 7	syl	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to G \in Grp$
35		simplrr	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to w \in X$
36	32 33 5	syl2anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to z \in X$
37		eqid	$⊢ -_{G} = -_{G}$
38	2 3 37	grppncan	$⊢ (G \in Grp \land w \in X \land z \in X) \to (w \underset{˙}{+} z) -_{G} z = w$
39	34 35 36 38	syl3anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to (w \underset{˙}{+} z) -_{G} z = w$
40		simpr	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to w \underset{˙}{+} z \in S$
41	37	subgsubcl	$⊢ (S \in SubGrp (G) \land w \underset{˙}{+} z \in S \land z \in S) \to (w \underset{˙}{+} z) -_{G} z \in S$
42	32 40 33 41	syl3anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to (w \underset{˙}{+} z) -_{G} z \in S$
43	39 42	eqeltrrd	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to w \in S$
44	3	subgcl	$⊢ (S \in SubGrp (G) \land z \in S \land w \in S) \to z \underset{˙}{+} w \in S$
45	32 33 43 44	syl3anc	$⊢ ((S \in SubGrp (G) \land (z \in S \land w \in X)) \land w \underset{˙}{+} z \in S) \to z \underset{˙}{+} w \in S$
46	31 45	impbida	$⊢ (S \in SubGrp (G) \land (z \in S \land w \in X)) \to (z \underset{˙}{+} w \in S \leftrightarrow w \underset{˙}{+} z \in S)$
47	46	anassrs	$⊢ ((S \in SubGrp (G) \land z \in S) \land w \in X) \to (z \underset{˙}{+} w \in S \leftrightarrow w \underset{˙}{+} z \in S)$
48	47	ralrimiva	$⊢ (S \in SubGrp (G) \land z \in S) \to \forall w \in X (z \underset{˙}{+} w \in S \leftrightarrow w \underset{˙}{+} z \in S)$
49	1	elnmz	$⊢ z \in N \leftrightarrow (z \in X \land \forall w \in X (z \underset{˙}{+} w \in S \leftrightarrow w \underset{˙}{+} z \in S))$
50	5 48 49	sylanbrc	$⊢ (S \in SubGrp (G) \land z \in S) \to z \in N$
51	50	ex	$⊢ S \in SubGrp (G) \to (z \in S \to z \in N)$
52	51	ssrdv	$⊢ S \in SubGrp (G) \to S \subseteq N$

Metamath Proof Explorer

Theorem ssnmz

Proof