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	sselid	$⊢ ((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	sselid	$⊢ ((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 21 25 26	grpcld	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to w \underset{˙}{+} u \in X$
31	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)$
32	22 30 31	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)$
33	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)$
34	21 25 26 23 33	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)$
35	34	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)$
36	2 3 21 26 23	grpcld	$⊢ ((G \in Grp \land z \in N \land w \in N) \land u \in X) \to u \underset{˙}{+} z \in X$
37	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)$
38	24 36 37	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)$
39	32 35 38	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)$
40	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)$
41	21 26 23 25 40	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)$
42	41	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)$
43	29 39 42	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)$
44	43	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)$
45	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))$
46	20 44 45	sylanbrc	$⊢ (G \in Grp \land z \in N \land w \in N) \to z \underset{˙}{+} w \in N$
47	46	3expa	$⊢ ((G \in Grp \land z \in N) \land w \in N) \to z \underset{˙}{+} w \in N$
48	47	ralrimiva	$⊢ (G \in Grp \land z \in N) \to \forall w \in N z \underset{˙}{+} w \in N$
49		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
50	2 49	grpinvcl	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \in X$
51	17 50	sylan2	$⊢ (G \in Grp \land z \in N) \to {inv}_{g} (G) (z) \in X$
52		simplr	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to z \in N$
53		simpll	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to G \in Grp$
54	51	adantr	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to {inv}_{g} (G) (z) \in X$
55		simpr	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to u \in X$
56	2 3 53 55 54	grpcld	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to u \underset{˙}{+} {inv}_{g} (G) (z) \in X$
57	2 3 53 54 56	grpcld	$⊢ ((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$
58	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)$
59	52 57 58	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)$
60	4 52	sselid	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to z \in X$
61	2 3 6 49	grprinv	$⊢ (G \in Grp \land z \in X) \to z \underset{˙}{+} {inv}_{g} (G) (z) = 0_{G}$
62	53 60 61	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to z \underset{˙}{+} {inv}_{g} (G) (z) = 0_{G}$
63	62	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))$
64	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)))$
65	53 60 54 56 64	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)))$
66	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)$
67	53 56 66	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)$
68	63 65 67	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)$
69	68	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)$
70	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)$
71	53 54 56 60 70	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)$
72	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)$
73	53 55 54 60 72	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)$
74	2 3 6 49	grplinv	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
75	53 60 74	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to {inv}_{g} (G) (z) \underset{˙}{+} z = 0_{G}$
76	75	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}$
77	2 3 6	grprid	$⊢ (G \in Grp \land u \in X) \to u \underset{˙}{+} 0_{G} = u$
78	53 55 77	syl2anc	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to u \underset{˙}{+} 0_{G} = u$
79	73 76 78	3eqtrd	$⊢ ((G \in Grp \land z \in N) \land u \in X) \to (u \underset{˙}{+} {inv}_{g} (G) (z)) \underset{˙}{+} z = u$
80	79	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$
81	71 80	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$
82	81	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)$
83	59 69 82	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)$
84	83	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)$
85	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))$
86	51 84 85	sylanbrc	$⊢ (G \in Grp \land z \in N) \to {inv}_{g} (G) (z) \in N$
87	48 86	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)$
88	87	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)$
89	2 3 49	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)))$
90	5 15 88 89	mpbir3and	$⊢ G \in Grp \to N \in SubGrp (G)$

Metamath Proof Explorer

Theorem nmzsubg

Proof