nmzsubg

Description: The normalizer N_G(S) of a subset S of the group is a subgroup. (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	nmzsubg	$⊢ G \in Grp \to N \in SubGrp (G)$

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	1	ssrab3	$⊢ N \subseteq X$
5	4	a1i	$⊢ G \in Grp \to N \subseteq X$
6		eqid	$⊢ 0_{G} = 0_{G}$
7	2 6	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
8	2 3 6	grplid	$⊢ (G \in Grp \land z \in X) \to 0_{G} \underset{˙}{+} z = z$
9	2 3 6	grprid	$⊢ (G \in Grp \land z \in X) \to z \underset{˙}{+} 0_{G} = z$
10	8 9	eqtr4d	$⊢ (G \in Grp \land z \in X) \to 0_{G} \underset{˙}{+} z = z \underset{˙}{+} 0_{G}$
11	10	eleq1d	$⊢ (G \in Grp \land z \in X) \to (0_{G} \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} 0_{G} \in S)$
12	11	ralrimiva	$⊢ G \in Grp \to \forall z \in X (0_{G} \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} 0_{G} \in S)$
13	1	elnmz	$⊢ 0_{G} \in N \leftrightarrow (0_{G} \in X \land \forall z \in X (0_{G} \underset{˙}{+} z \in S \leftrightarrow z \underset{˙}{+} 0_{G} \in S))$
14	7 12 13	sylanbrc	$⊢ G \in Grp \to 0_{G} \in N$
15	14	ne0d	$⊢ G \in Grp \to N \neq \emptyset$
16		id	$⊢ G \in Grp \to G \in Grp$
17	4	sseli	$⊢ z \in N \to z \in X$
18	4	sseli	$⊢ w \in N \to w \in X$
19	2 3	grpcl	$⊢ (G \in Grp \land z \in X \land w \in X) \to z \underset{˙}{+} w \in X$
20	16 17 18 19	syl3an	$⊢ (G \in Grp \land z \in N \land w \in N) \to z \underset{˙}{+} w \in X$
21		simpl1	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to G \in Grp$
22		simpl2	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to z \in N$
23	4 22	sseldi	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to z \in X$
24		simpl3	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to w \in N$
25	4 24	sseldi	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to w \in X$
26		simpr	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to u \in X$
27	2 3	grpass	$⊢ (G \in Grp \land (z \in X \land w \in X \land u \in X)) \to (z \underset{˙}{+} w) \underset{˙}{+} u = z \underset{˙}{+} (w \underset{˙}{+} u)$
28	21 23 25 26 27	syl13anc	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to (z \underset{˙}{+} w) \underset{˙}{+} u = z \underset{˙}{+} (w \underset{˙}{+} u)$
29	28	eleq1d	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to ((z \underset{˙}{+} w) \underset{˙}{+} u \in S \leftrightarrow z \underset{˙}{+} (w \underset{˙}{+} u) \in S)$
30	2 3	grpcl	$⊢ (G \in Grp \land w \in X \land u \in X) \to w \underset{˙}{+} u \in X$
31	21 25 26 30	syl3anc	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to w \underset{˙}{+} u \in X$
32	1	nmzbi	$⊢ (z \in N \land w \underset{˙}{+} u \in X) \to (z \underset{˙}{+} (w \underset{˙}{+} u) \in S \leftrightarrow (w \underset{˙}{+} u) \underset{˙}{+} z \in S)$
33	22 31 32	syl2anc	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to (z \underset{˙}{+} (w \underset{˙}{+} u) \in S \leftrightarrow (w \underset{˙}{+} u) \underset{˙}{+} z \in S)$
34	2 3	grpass	$⊢ (G \in Grp \land (w \in X \land u \in X \land z \in X)) \to (w \underset{˙}{+} u) \underset{˙}{+} z = w \underset{˙}{+} (u \underset{˙}{+} z)$
35	21 25 26 23 34	syl13anc	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to (w \underset{˙}{+} u) \underset{˙}{+} z = w \underset{˙}{+} (u \underset{˙}{+} z)$
36	35	eleq1d	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to ((w \underset{˙}{+} u) \underset{˙}{+} z \in S \leftrightarrow w \underset{˙}{+} (u \underset{˙}{+} z) \in S)$
37	2 3	grpcl	$⊢ (G \in Grp \land u \in X \land z \in X) \to u \underset{˙}{+} z \in X$
38	21 26 23 37	syl3anc	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to u \underset{˙}{+} z \in X$
39	1	nmzbi	$⊢ (w \in N \land u \underset{˙}{+} z \in X) \to (w \underset{˙}{+} (u \underset{˙}{+} z) \in S \leftrightarrow (u \underset{˙}{+} z) \underset{˙}{+} w \in S)$
40	24 38 39	syl2anc	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to (w \underset{˙}{+} (u \underset{˙}{+} z) \in S \leftrightarrow (u \underset{˙}{+} z) \underset{˙}{+} w \in S)$
41	33 36 40	3bitrd	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to (z \underset{˙}{+} (w \underset{˙}{+} u) \in S \leftrightarrow (u \underset{˙}{+} z) \underset{˙}{+} w \in S)$
42	2 3	grpass	$⊢ (G \in Grp \land (u \in X \land z \in X \land w \in X)) \to (u \underset{˙}{+} z) \underset{˙}{+} w = u \underset{˙}{+} (z \underset{˙}{+} w)$
43	21 26 23 25 42	syl13anc	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to (u \underset{˙}{+} z) \underset{˙}{+} w = u \underset{˙}{+} (z \underset{˙}{+} w)$
44	43	eleq1d	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to ((u \underset{˙}{+} z) \underset{˙}{+} w \in S \leftrightarrow u \underset{˙}{+} (z \underset{˙}{+} w) \in S)$
45	29 41 44	3bitrd	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to ((z \underset{˙}{+} w) \underset{˙}{+} u \in S \leftrightarrow u \underset{˙}{+} (z \underset{˙}{+} w) \in S)$
46	45	ralrimiva	$⊢ (G \in Grp \land z \in N \land w \in N) \to \forall u \in X ((z \underset{˙}{+} w) \underset{˙}{+} u \in S \leftrightarrow u \underset{˙}{+} (z \underset{˙}{+} w) \in S)$
47	1	elnmz	$⊢ z \underset{˙}{+} w \in N \leftrightarrow (z \underset{˙}{+} w \in X \land \forall u \in X ((z \underset{˙}{+} w) \underset{˙}{+} u \in S \leftrightarrow u \underset{˙}{+} (z \underset{˙}{+} w) \in S))$
48	20 46 47	sylanbrc	$⊢ (G \in Grp \land z \in N \land w \in N) \to z \underset{˙}{+} w \in N$
49	48	3expa	$⊢ ((G \in Grp \land z \in N) \land w \in N) \to z \underset{˙}{+} w \in N$
50	49	ralrimiva	$⊢ (G \in Grp \land z \in N) \to \forall w \in N z \underset{˙}{+} w \in N$
51		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
52	2 51	grpinvcl	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \in X$
53	17 52	sylan2	$⊢ (G \in Grp \land z \in N) \to {inv}_{g} (G) (z) \in X$
54		simplr	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to z \in N$
55		simpll	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to G \in Grp$
56	53	adantr	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to {inv}_{g} (G) (z) \in X$
57		simpr	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to u \in X$
58	2 3	grpcl	$⊢ (G \in Grp \land u \in X \land {inv}_{g} (G) (z) \in X) \to u \underset{˙}{+} {inv}_{g} (G) (z) \in X$
59	55 57 56 58	syl3anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to u \underset{˙}{+} {inv}_{g} (G) (z) \in X$
60	2 3	grpcl	$⊢ (G \in Grp \land {inv}_{g} (G) (z) \in X \land u \underset{˙}{+} {inv}_{g} (G) (z) \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) \in X$
61	55 56 59 60	syl3anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) \in X$
62	1	nmzbi	$⊢ (z \in N \land {inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) \in X) \to (z \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \in S \leftrightarrow ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \underset{˙}{+} z \in S)$
63	54 61 62	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (z \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \in S \leftrightarrow ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \underset{˙}{+} z \in S)$
64	4 54	sseldi	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to z \in X$
65	2 3 6 51	grprinv	$⊢ (G \in Grp \land z \in X) \to z \underset{˙}{+} {inv}_{g} (G) (z) = 0_{G}$
66	55 64 65	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to z \underset{˙}{+} {inv}_{g} (G) (z) = 0_{G}$
67	66	oveq1d	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (z \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) = 0_{G} \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))$
68	2 3	grpass	$⊢ (G \in Grp \land (z \in X \land {inv}_{g} (G) (z) \in X \land u \underset{˙}{+} {inv}_{g} (G) (z) \in X)) \to (z \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) = z \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)))$
69	55 64 56 59 68	syl13anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (z \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) = z \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)))$
70	2 3 6	grplid	$⊢ (G \in Grp \land u \underset{˙}{+} {inv}_{g} (G) (z) \in X) \to 0_{G} \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) = u \underset{˙}{+} {inv}_{g} (G) (z)$
71	55 59 70	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to 0_{G} \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z)) = u \underset{˙}{+} {inv}_{g} (G) (z)$
72	67 69 71	3eqtr3d	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to z \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) = u \underset{˙}{+} {inv}_{g} (G) (z)$
73	72	eleq1d	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (z \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \in S \leftrightarrow u \underset{˙}{+} {inv}_{g} (G) (z) \in S)$
74	2 3	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (z) \in X \land u \underset{˙}{+} {inv}_{g} (G) (z) \in X \land z \in X)) \to ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \underset{˙}{+} z = {inv}_{g} (G) (z) \underset{˙}{+} ((u \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} z)$
75	55 56 59 64 74	syl13anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \underset{˙}{+} z = {inv}_{g} (G) (z) \underset{˙}{+} ((u \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} z)$
76	2 3	grpass	$⊢ (G \in Grp \land (u \in X \land {inv}_{g} (G) (z) \in X \land z \in X)) \to (u \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} z = u \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} z)$
77	55 57 56 64 76	syl13anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (u \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} z = u \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} z)$
78	2 3 6 51	grplinv	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
79	55 64 78	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
80	79	oveq2d	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to u \underset{˙}{+} ({inv}_{g} (G) (z) \underset{˙}{+} z) = u \underset{˙}{+} 0_{G}$
81	2 3 6	grprid	$⊢ (G \in Grp \land u \in X) \to u \underset{˙}{+} 0_{G} = u$
82	55 57 81	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to u \underset{˙}{+} 0_{G} = u$
83	77 80 82	3eqtrd	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (u \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} z = u$
84	83	oveq2d	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} ((u \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} z) = {inv}_{g} (G) (z) \underset{˙}{+} u$
85	75 84	eqtrd	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to ({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \underset{˙}{+} z = {inv}_{g} (G) (z) \underset{˙}{+} u$
86	85	eleq1d	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (({inv}_{g} (G) (z) \underset{˙}{+} (u \underset{˙}{+} {inv}_{g} (G) (z))) \underset{˙}{+} z \in S \leftrightarrow {inv}_{g} (G) (z) \underset{˙}{+} u \in S)$
87	63 73 86	3bitr3rd	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to ({inv}_{g} (G) (z) \underset{˙}{+} u \in S \leftrightarrow u \underset{˙}{+} {inv}_{g} (G) (z) \in S)$
88	87	ralrimiva	$⊢ (G \in Grp \land z \in N) \to \forall u \in X ({inv}_{g} (G) (z) \underset{˙}{+} u \in S \leftrightarrow u \underset{˙}{+} {inv}_{g} (G) (z) \in S)$
89	1	elnmz	$⊢ {inv}_{g} (G) (z) \in N \leftrightarrow ({inv}_{g} (G) (z) \in X \land \forall u \in X ({inv}_{g} (G) (z) \underset{˙}{+} u \in S \leftrightarrow u \underset{˙}{+} {inv}_{g} (G) (z) \in S))$
90	53 88 89	sylanbrc	$⊢ (G \in Grp \land z \in N) \to {inv}_{g} (G) (z) \in N$
91	50 90	jca	$⊢ (G \in Grp \land z \in N) \to (\forall w \in N z \underset{˙}{+} w \in N \land {inv}_{g} (G) (z) \in N)$
92	91	ralrimiva	$⊢ G \in Grp \to \forall z \in N (\forall w \in N z \underset{˙}{+} w \in N \land {inv}_{g} (G) (z) \in N)$
93	2 3 51	issubg2	$⊢ G \in Grp \to (N \in SubGrp (G) \leftrightarrow (N \subseteq X \land N \neq \emptyset \land \forall z \in N (\forall w \in N z \underset{˙}{+} w \in N \land {inv}_{g} (G) (z) \in N)))$
94	5 15 92 93	mpbir3and	$⊢ G \in Grp \to N \in SubGrp (G)$

Metamath Proof Explorer

Theorem nmzsubg

Proof