sylow3lem2

Description: Lemma for sylow3 , first part. The stabilizer of a given Sylow subgroup K in the group action .(+) acting on all of G is the normalizer N_G(K). (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	sylow3.x	$⊢ X = {Base}_{G}$
	sylow3.g	$⊢ φ \to G \in Grp$
	sylow3.xf	$⊢ φ \to X \in Fin$
	sylow3.p	$⊢ φ \to P \in ℙ$
	sylow3lem1.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow3lem1.d	$⊢ \underset{˙}{-} = -_{G}$
	sylow3lem1.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
	sylow3lem2.k	$⊢ φ \to K \in (P pSyl G)$
	sylow3lem2.h	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} K = K\}$
	sylow3lem2.n	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in K \leftrightarrow y \underset{˙}{+} x \in K)\}$
Assertion	sylow3lem2	$⊢ φ \to H = N$

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	$⊢ X = {Base}_{G}$
2		sylow3.g	$⊢ φ \to G \in Grp$
3		sylow3.xf	$⊢ φ \to X \in Fin$
4		sylow3.p	$⊢ φ \to P \in ℙ$
5		sylow3lem1.a	$⊢ \underset{˙}{+} = +_{G}$
6		sylow3lem1.d	$⊢ \underset{˙}{-} = -_{G}$
7		sylow3lem1.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
8		sylow3lem2.k	$⊢ φ \to K \in (P pSyl G)$
9		sylow3lem2.h	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} K = K\}$
10		sylow3lem2.n	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in K \leftrightarrow y \underset{˙}{+} x \in K)\}$
11	10	ssrab3	$⊢ N \subseteq X$
12		sseqin2	$⊢ N \subseteq X \leftrightarrow X \cap N = N$
13	11 12	mpbi	$⊢ X \cap N = N$
14		simpr	$⊢ (φ \land u \in X) \to u \in X$
15	8	adantr	$⊢ (φ \land u \in X) \to K \in (P pSyl G)$
16		mptexg	$⊢ K \in (P pSyl G) \to (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V$
17		rnexg	$⊢ (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V \to ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V$
18	15 16 17	3syl	$⊢ (φ \land u \in X) \to ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V$
19		simpr	$⊢ (x = u \land y = K) \to y = K$
20		simpl	$⊢ (x = u \land y = K) \to x = u$
21	20	oveq1d	$⊢ (x = u \land y = K) \to x \underset{˙}{+} z = u \underset{˙}{+} z$
22	21 20	oveq12d	$⊢ (x = u \land y = K) \to (x \underset{˙}{+} z) \underset{˙}{-} x = (u \underset{˙}{+} z) \underset{˙}{-} u$
23	19 22	mpteq12dv	$⊢ (x = u \land y = K) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
24	23	rneqd	$⊢ (x = u \land y = K) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
25	24 7	ovmpoga	$⊢ (u \in X \land K \in (P pSyl G) \land ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V) \to u \underset{˙}{\oplus} K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
26	14 15 18 25	syl3anc	$⊢ (φ \land u \in X) \to u \underset{˙}{\oplus} K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
27	26	adantr	$⊢ ((φ \land u \in X) \land u \in N) \to u \underset{˙}{\oplus} K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
28		slwsubg	$⊢ K \in (P pSyl G) \to K \in SubGrp (G)$
29	8 28	syl	$⊢ φ \to K \in SubGrp (G)$
30	29	adantr	$⊢ (φ \land u \in X) \to K \in SubGrp (G)$
31		eqid	$⊢ (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) = (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
32	1 5 6 31 10	conjnmz	$⊢ (K \in SubGrp (G) \land u \in N) \to K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
33	30 32	sylan	$⊢ ((φ \land u \in X) \land u \in N) \to K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
34	27 33	eqtr4d	$⊢ ((φ \land u \in X) \land u \in N) \to u \underset{˙}{\oplus} K = K$
35		simplr	$⊢ ((φ \land u \in X) \land u \underset{˙}{\oplus} K = K) \to u \in X$
36		simprl	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to u \underset{˙}{\oplus} K = K$
37	26	adantr	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to u \underset{˙}{\oplus} K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
38	36 37	eqtr3d	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
39	38	eleq2d	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to (u \underset{˙}{+} w \in K \leftrightarrow u \underset{˙}{+} w \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u))$
40		ovex	$⊢ u \underset{˙}{+} w \in V$
41		eqeq1	$⊢ v = u \underset{˙}{+} w \to (v = (u \underset{˙}{+} z) \underset{˙}{-} u \leftrightarrow u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)$
42	41	rexbidv	$⊢ v = u \underset{˙}{+} w \to (\exists z \in K v = (u \underset{˙}{+} z) \underset{˙}{-} u \leftrightarrow \exists z \in K u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)$
43	31	rnmpt	$⊢ ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) = \{v \| \exists z \in K v = (u \underset{˙}{+} z) \underset{˙}{-} u\}$
44	40 42 43	elab2	$⊢ u \underset{˙}{+} w \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \leftrightarrow \exists z \in K u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u$
45		simprr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u$
46	2	ad3antrrr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to G \in Grp$
47		simpllr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to u \in X$
48	1	subgss	$⊢ K \in SubGrp (G) \to K \subseteq X$
49	29 48	syl	$⊢ φ \to K \subseteq X$
50	49	ad3antrrr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to K \subseteq X$
51		simprl	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to z \in K$
52	50 51	sseldd	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to z \in X$
53	1 5 6	grpaddsubass	$⊢ (G \in Grp \land (u \in X \land z \in X \land u \in X)) \to (u \underset{˙}{+} z) \underset{˙}{-} u = u \underset{˙}{+} (z \underset{˙}{-} u)$
54	46 47 52 47 53	syl13anc	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to (u \underset{˙}{+} z) \underset{˙}{-} u = u \underset{˙}{+} (z \underset{˙}{-} u)$
55	45 54	eqtr2d	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to u \underset{˙}{+} (z \underset{˙}{-} u) = u \underset{˙}{+} w$
56	1 6	grpsubcl	$⊢ (G \in Grp \land z \in X \land u \in X) \to z \underset{˙}{-} u \in X$
57	46 52 47 56	syl3anc	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to z \underset{˙}{-} u \in X$
58		simplrr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to w \in X$
59	1 5	grplcan	$⊢ (G \in Grp \land (z \underset{˙}{-} u \in X \land w \in X \land u \in X)) \to (u \underset{˙}{+} (z \underset{˙}{-} u) = u \underset{˙}{+} w \leftrightarrow z \underset{˙}{-} u = w)$
60	46 57 58 47 59	syl13anc	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to (u \underset{˙}{+} (z \underset{˙}{-} u) = u \underset{˙}{+} w \leftrightarrow z \underset{˙}{-} u = w)$
61	55 60	mpbid	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to z \underset{˙}{-} u = w$
62	1 5 6	grpsubadd	$⊢ (G \in Grp \land (z \in X \land u \in X \land w \in X)) \to (z \underset{˙}{-} u = w \leftrightarrow w \underset{˙}{+} u = z)$
63	46 52 47 58 62	syl13anc	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to (z \underset{˙}{-} u = w \leftrightarrow w \underset{˙}{+} u = z)$
64	61 63	mpbid	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to w \underset{˙}{+} u = z$
65	64 51	eqeltrd	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land (z \in K \land u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u)) \to w \underset{˙}{+} u \in K$
66	65	rexlimdvaa	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to (\exists z \in K u \underset{˙}{+} w = (u \underset{˙}{+} z) \underset{˙}{-} u \to w \underset{˙}{+} u \in K)$
67	44 66	syl5bi	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to (u \underset{˙}{+} w \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \to w \underset{˙}{+} u \in K)$
68		simpr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to w \underset{˙}{+} u \in K$
69		oveq2	$⊢ z = w \underset{˙}{+} u \to u \underset{˙}{+} z = u \underset{˙}{+} (w \underset{˙}{+} u)$
70	69	oveq1d	$⊢ z = w \underset{˙}{+} u \to (u \underset{˙}{+} z) \underset{˙}{-} u = (u \underset{˙}{+} (w \underset{˙}{+} u)) \underset{˙}{-} u$
71		ovex	$⊢ (u \underset{˙}{+} (w \underset{˙}{+} u)) \underset{˙}{-} u \in V$
72	70 31 71	fvmpt	$⊢ w \underset{˙}{+} u \in K \to (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) (w \underset{˙}{+} u) = (u \underset{˙}{+} (w \underset{˙}{+} u)) \underset{˙}{-} u$
73	68 72	syl	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) (w \underset{˙}{+} u) = (u \underset{˙}{+} (w \underset{˙}{+} u)) \underset{˙}{-} u$
74	2	ad3antrrr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to G \in Grp$
75		simpllr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to u \in X$
76		simplrr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to w \in X$
77	1 5	grpass	$⊢ (G \in Grp \land (u \in X \land w \in X \land u \in X)) \to (u \underset{˙}{+} w) \underset{˙}{+} u = u \underset{˙}{+} (w \underset{˙}{+} u)$
78	74 75 76 75 77	syl13anc	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to (u \underset{˙}{+} w) \underset{˙}{+} u = u \underset{˙}{+} (w \underset{˙}{+} u)$
79	78	oveq1d	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to ((u \underset{˙}{+} w) \underset{˙}{+} u) \underset{˙}{-} u = (u \underset{˙}{+} (w \underset{˙}{+} u)) \underset{˙}{-} u$
80	1 5	grpcl	$⊢ (G \in Grp \land u \in X \land w \in X) \to u \underset{˙}{+} w \in X$
81	74 75 76 80	syl3anc	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to u \underset{˙}{+} w \in X$
82	1 5 6	grppncan	$⊢ (G \in Grp \land u \underset{˙}{+} w \in X \land u \in X) \to ((u \underset{˙}{+} w) \underset{˙}{+} u) \underset{˙}{-} u = u \underset{˙}{+} w$
83	74 81 75 82	syl3anc	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to ((u \underset{˙}{+} w) \underset{˙}{+} u) \underset{˙}{-} u = u \underset{˙}{+} w$
84	73 79 83	3eqtr2d	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) (w \underset{˙}{+} u) = u \underset{˙}{+} w$
85		ovex	$⊢ (u \underset{˙}{+} z) \underset{˙}{-} u \in V$
86	85 31	fnmpti	$⊢ (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) Fn K$
87		fnfvelrn	$⊢ ((z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) Fn K \land w \underset{˙}{+} u \in K) \to (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) (w \underset{˙}{+} u) \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
88	86 68 87	sylancr	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) (w \underset{˙}{+} u) \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
89	84 88	eqeltrrd	$⊢ (((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \land w \underset{˙}{+} u \in K) \to u \underset{˙}{+} w \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
90	89	ex	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to (w \underset{˙}{+} u \in K \to u \underset{˙}{+} w \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u))$
91	67 90	impbid	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to (u \underset{˙}{+} w \in ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \leftrightarrow w \underset{˙}{+} u \in K)$
92	39 91	bitrd	$⊢ ((φ \land u \in X) \land (u \underset{˙}{\oplus} K = K \land w \in X)) \to (u \underset{˙}{+} w \in K \leftrightarrow w \underset{˙}{+} u \in K)$
93	92	anassrs	$⊢ (((φ \land u \in X) \land u \underset{˙}{\oplus} K = K) \land w \in X) \to (u \underset{˙}{+} w \in K \leftrightarrow w \underset{˙}{+} u \in K)$
94	93	ralrimiva	$⊢ ((φ \land u \in X) \land u \underset{˙}{\oplus} K = K) \to \forall w \in X (u \underset{˙}{+} w \in K \leftrightarrow w \underset{˙}{+} u \in K)$
95	10	elnmz	$⊢ u \in N \leftrightarrow (u \in X \land \forall w \in X (u \underset{˙}{+} w \in K \leftrightarrow w \underset{˙}{+} u \in K))$
96	35 94 95	sylanbrc	$⊢ ((φ \land u \in X) \land u \underset{˙}{\oplus} K = K) \to u \in N$
97	34 96	impbida	$⊢ (φ \land u \in X) \to (u \in N \leftrightarrow u \underset{˙}{\oplus} K = K)$
98	97	rabbi2dva	$⊢ φ \to X \cap N = \{u \in X \| u \underset{˙}{\oplus} K = K\}$
99	13 98	eqtr3id	$⊢ φ \to N = \{u \in X \| u \underset{˙}{\oplus} K = K\}$
100	9 99	eqtr4id	$⊢ φ \to H = N$

Metamath Proof Explorer

Theorem sylow3lem2

Proof