sylow3lem1

Description: Lemma for sylow3 , first part. (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))$
Assertion	sylow3lem1	$⊢ φ \to \underset{˙}{\oplus} \in (G GrpAct (P pSyl G))$

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		ovex	$⊢ P pSyl G \in V$
9	2 8	jctir	$⊢ φ \to (G \in Grp \land P pSyl G \in V)$
10	1	fislw	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to (y \in (P pSyl G) \leftrightarrow (y \in SubGrp (G) \land \|y\| = P^{P pCnt \|X\|}))$
11	2 3 4 10	syl3anc	$⊢ φ \to (y \in (P pSyl G) \leftrightarrow (y \in SubGrp (G) \land \|y\| = P^{P pCnt \|X\|}))$
12	11	biimpa	$⊢ (φ \land y \in (P pSyl G)) \to (y \in SubGrp (G) \land \|y\| = P^{P pCnt \|X\|})$
13	12	adantrl	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to (y \in SubGrp (G) \land \|y\| = P^{P pCnt \|X\|})$
14	13	simpld	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to y \in SubGrp (G)$
15		simprl	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to x \in X$
16		eqid	$⊢ (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)$
17	1 5 6 16	conjsubg	$⊢ (y \in SubGrp (G) \land x \in X) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in SubGrp (G)$
18	14 15 17	syl2anc	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in SubGrp (G)$
19	1 5 6 16	conjsubgen	$⊢ (y \in SubGrp (G) \land x \in X) \to y \approx ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)$
20	14 15 19	syl2anc	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to y \approx ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)$
21	3	adantr	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to X \in Fin$
22	1	subgss	$⊢ y \in SubGrp (G) \to y \subseteq X$
23	14 22	syl	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to y \subseteq X$
24	21 23	ssfid	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to y \in Fin$
25	1	subgss	$⊢ ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in SubGrp (G) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \subseteq X$
26	18 25	syl	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \subseteq X$
27	21 26	ssfid	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in Fin$
28		hashen	$⊢ (y \in Fin \land ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in Fin) \to (\|y\| = \|ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)\| \leftrightarrow y \approx ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
29	24 27 28	syl2anc	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to (\|y\| = \|ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)\| \leftrightarrow y \approx ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
30	20 29	mpbird	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to \|y\| = \|ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)\|$
31	13	simprd	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to \|y\| = P^{P pCnt \|X\|}$
32	30 31	eqtr3d	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to \|ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)\| = P^{P pCnt \|X\|}$
33	1	fislw	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to (ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in (P pSyl G) \leftrightarrow (ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in SubGrp (G) \land \|ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)\| = P^{P pCnt \|X\|}))$
34	2 3 4 33	syl3anc	$⊢ φ \to (ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in (P pSyl G) \leftrightarrow (ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in SubGrp (G) \land \|ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)\| = P^{P pCnt \|X\|}))$
35	34	adantr	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to (ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in (P pSyl G) \leftrightarrow (ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in SubGrp (G) \land \|ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x)\| = P^{P pCnt \|X\|}))$
36	18 32 35	mpbir2and	$⊢ (φ \land (x \in X \land y \in (P pSyl G))) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in (P pSyl G)$
37	36	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in (P pSyl G) ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in (P pSyl G)$
38	7	fmpo	$⊢ \forall x \in X \forall y \in (P pSyl G) ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) \in (P pSyl G) \leftrightarrow \underset{˙}{\oplus} : X \times (P pSyl G) ⟶ P pSyl G$
39	37 38	sylib	$⊢ φ \to \underset{˙}{\oplus} : X \times (P pSyl G) ⟶ P pSyl G$
40	2	adantr	$⊢ (φ \land a \in (P pSyl G)) \to G \in Grp$
41		eqid	$⊢ 0_{G} = 0_{G}$
42	1 41	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
43	40 42	syl	$⊢ (φ \land a \in (P pSyl G)) \to 0_{G} \in X$
44		simpr	$⊢ (φ \land a \in (P pSyl G)) \to a \in (P pSyl G)$
45		simpr	$⊢ (x = 0_{G} \land y = a) \to y = a$
46		simpl	$⊢ (x = 0_{G} \land y = a) \to x = 0_{G}$
47	46	oveq1d	$⊢ (x = 0_{G} \land y = a) \to x \underset{˙}{+} z = 0_{G} \underset{˙}{+} z$
48	47 46	oveq12d	$⊢ (x = 0_{G} \land y = a) \to (x \underset{˙}{+} z) \underset{˙}{-} x = (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G}$
49	45 48	mpteq12dv	$⊢ (x = 0_{G} \land y = a) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G})$
50	49	rneqd	$⊢ (x = 0_{G} \land y = a) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = ran (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G})$
51		vex	$⊢ a \in V$
52	51	mptex	$⊢ (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G}) \in V$
53	52	rnex	$⊢ ran (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G}) \in V$
54	50 7 53	ovmpoa	$⊢ (0_{G} \in X \land a \in (P pSyl G)) \to 0_{G} \underset{˙}{\oplus} a = ran (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G})$
55	43 44 54	syl2anc	$⊢ (φ \land a \in (P pSyl G)) \to 0_{G} \underset{˙}{\oplus} a = ran (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G})$
56	2	ad2antrr	$⊢ ((φ \land a \in (P pSyl G)) \land z \in a) \to G \in Grp$
57		slwsubg	$⊢ a \in (P pSyl G) \to a \in SubGrp (G)$
58	57	adantl	$⊢ (φ \land a \in (P pSyl G)) \to a \in SubGrp (G)$
59	1	subgss	$⊢ a \in SubGrp (G) \to a \subseteq X$
60	58 59	syl	$⊢ (φ \land a \in (P pSyl G)) \to a \subseteq X$
61	60	sselda	$⊢ ((φ \land a \in (P pSyl G)) \land z \in a) \to z \in X$
62	1 5 41	grplid	$⊢ (G \in Grp \land z \in X) \to 0_{G} \underset{˙}{+} z = z$
63	56 61 62	syl2anc	$⊢ ((φ \land a \in (P pSyl G)) \land z \in a) \to 0_{G} \underset{˙}{+} z = z$
64	63	oveq1d	$⊢ ((φ \land a \in (P pSyl G)) \land z \in a) \to (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G} = z \underset{˙}{-} 0_{G}$
65	1 41 6	grpsubid1	$⊢ (G \in Grp \land z \in X) \to z \underset{˙}{-} 0_{G} = z$
66	56 61 65	syl2anc	$⊢ ((φ \land a \in (P pSyl G)) \land z \in a) \to z \underset{˙}{-} 0_{G} = z$
67	64 66	eqtrd	$⊢ ((φ \land a \in (P pSyl G)) \land z \in a) \to (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G} = z$
68	67	mpteq2dva	$⊢ (φ \land a \in (P pSyl G)) \to (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G}) = (z \in a ⟼ z)$
69		mptresid	$⊢ {I ↾}_{a} = (z \in a ⟼ z)$
70	68 69	eqtr4di	$⊢ (φ \land a \in (P pSyl G)) \to (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G}) = {I ↾}_{a}$
71	70	rneqd	$⊢ (φ \land a \in (P pSyl G)) \to ran (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G}) = ran ({I ↾}_{a})$
72		rnresi	$⊢ ran ({I ↾}_{a}) = a$
73	71 72	eqtrdi	$⊢ (φ \land a \in (P pSyl G)) \to ran (z \in a ⟼ (0_{G} \underset{˙}{+} z) \underset{˙}{-} 0_{G}) = a$
74	55 73	eqtrd	$⊢ (φ \land a \in (P pSyl G)) \to 0_{G} \underset{˙}{\oplus} a = a$
75		ovex	$⊢ (c \underset{˙}{+} z) \underset{˙}{-} c \in V$
76		oveq2	$⊢ w = (c \underset{˙}{+} z) \underset{˙}{-} c \to b \underset{˙}{+} w = b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)$
77	76	oveq1d	$⊢ w = (c \underset{˙}{+} z) \underset{˙}{-} c \to (b \underset{˙}{+} w) \underset{˙}{-} b = (b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)) \underset{˙}{-} b$
78	75 77	abrexco	$⊢ \{u \| \exists w \in \{v \| \exists z \in a v = (c \underset{˙}{+} z) \underset{˙}{-} c\} u = (b \underset{˙}{+} w) \underset{˙}{-} b\} = \{u \| \exists z \in a u = (b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)) \underset{˙}{-} b\}$
79		simprr	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to c \in X$
80		simplr	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to a \in (P pSyl G)$
81		simpr	$⊢ (x = c \land y = a) \to y = a$
82		simpl	$⊢ (x = c \land y = a) \to x = c$
83	82	oveq1d	$⊢ (x = c \land y = a) \to x \underset{˙}{+} z = c \underset{˙}{+} z$
84	83 82	oveq12d	$⊢ (x = c \land y = a) \to (x \underset{˙}{+} z) \underset{˙}{-} x = (c \underset{˙}{+} z) \underset{˙}{-} c$
85	81 84	mpteq12dv	$⊢ (x = c \land y = a) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c)$
86	85	rneqd	$⊢ (x = c \land y = a) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = ran (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c)$
87	51	mptex	$⊢ (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c) \in V$
88	87	rnex	$⊢ ran (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c) \in V$
89	86 7 88	ovmpoa	$⊢ (c \in X \land a \in (P pSyl G)) \to c \underset{˙}{\oplus} a = ran (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c)$
90	79 80 89	syl2anc	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to c \underset{˙}{\oplus} a = ran (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c)$
91		eqid	$⊢ (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c) = (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c)$
92	91	rnmpt	$⊢ ran (z \in a ⟼ (c \underset{˙}{+} z) \underset{˙}{-} c) = \{v \| \exists z \in a v = (c \underset{˙}{+} z) \underset{˙}{-} c\}$
93	90 92	eqtrdi	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to c \underset{˙}{\oplus} a = \{v \| \exists z \in a v = (c \underset{˙}{+} z) \underset{˙}{-} c\}$
94	93	rexeqdv	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to (\exists w \in (c \underset{˙}{\oplus} a) u = (b \underset{˙}{+} w) \underset{˙}{-} b \leftrightarrow \exists w \in \{v \| \exists z \in a v = (c \underset{˙}{+} z) \underset{˙}{-} c\} u = (b \underset{˙}{+} w) \underset{˙}{-} b)$
95	94	abbidv	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to \{u \| \exists w \in (c \underset{˙}{\oplus} a) u = (b \underset{˙}{+} w) \underset{˙}{-} b\} = \{u \| \exists w \in \{v \| \exists z \in a v = (c \underset{˙}{+} z) \underset{˙}{-} c\} u = (b \underset{˙}{+} w) \underset{˙}{-} b\}$
96	40	adantr	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to G \in Grp$
97	96	adantr	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to G \in Grp$
98		simprl	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to b \in X$
99	1 5	grpcl	$⊢ (G \in Grp \land b \in X \land c \in X) \to b \underset{˙}{+} c \in X$
100	96 98 79 99	syl3anc	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to b \underset{˙}{+} c \in X$
101	100	adantr	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to b \underset{˙}{+} c \in X$
102	61	adantlr	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to z \in X$
103	1 5	grpcl	$⊢ (G \in Grp \land b \underset{˙}{+} c \in X \land z \in X) \to (b \underset{˙}{+} c) \underset{˙}{+} z \in X$
104	97 101 102 103	syl3anc	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to (b \underset{˙}{+} c) \underset{˙}{+} z \in X$
105	79	adantr	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to c \in X$
106	98	adantr	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to b \in X$
107	1 5 6	grpsubsub4	$⊢ (G \in Grp \land ((b \underset{˙}{+} c) \underset{˙}{+} z \in X \land c \in X \land b \in X)) \to (((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} c) \underset{˙}{-} b = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)$
108	97 104 105 106 107	syl13anc	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to (((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} c) \underset{˙}{-} b = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)$
109	1 5	grpass	$⊢ (G \in Grp \land (b \in X \land c \in X \land z \in X)) \to (b \underset{˙}{+} c) \underset{˙}{+} z = b \underset{˙}{+} (c \underset{˙}{+} z)$
110	97 106 105 102 109	syl13anc	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to (b \underset{˙}{+} c) \underset{˙}{+} z = b \underset{˙}{+} (c \underset{˙}{+} z)$
111	110	oveq1d	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} c = (b \underset{˙}{+} (c \underset{˙}{+} z)) \underset{˙}{-} c$
112	1 5	grpcl	$⊢ (G \in Grp \land c \in X \land z \in X) \to c \underset{˙}{+} z \in X$
113	97 105 102 112	syl3anc	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to c \underset{˙}{+} z \in X$
114	1 5 6	grpaddsubass	$⊢ (G \in Grp \land (b \in X \land c \underset{˙}{+} z \in X \land c \in X)) \to (b \underset{˙}{+} (c \underset{˙}{+} z)) \underset{˙}{-} c = b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)$
115	97 106 113 105 114	syl13anc	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to (b \underset{˙}{+} (c \underset{˙}{+} z)) \underset{˙}{-} c = b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)$
116	111 115	eqtrd	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} c = b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)$
117	116	oveq1d	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to (((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} c) \underset{˙}{-} b = (b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)) \underset{˙}{-} b$
118	108 117	eqtr3d	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c) = (b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)) \underset{˙}{-} b$
119	118	eqeq2d	$⊢ (((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \land z \in a) \to (u = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c) \leftrightarrow u = (b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)) \underset{˙}{-} b)$
120	119	rexbidva	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to (\exists z \in a u = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c) \leftrightarrow \exists z \in a u = (b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)) \underset{˙}{-} b)$
121	120	abbidv	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to \{u \| \exists z \in a u = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)\} = \{u \| \exists z \in a u = (b \underset{˙}{+} ((c \underset{˙}{+} z) \underset{˙}{-} c)) \underset{˙}{-} b\}$
122	78 95 121	3eqtr4a	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to \{u \| \exists w \in (c \underset{˙}{\oplus} a) u = (b \underset{˙}{+} w) \underset{˙}{-} b\} = \{u \| \exists z \in a u = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)\}$
123		eqid	$⊢ (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b) = (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b)$
124	123	rnmpt	$⊢ ran (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b) = \{u \| \exists w \in (c \underset{˙}{\oplus} a) u = (b \underset{˙}{+} w) \underset{˙}{-} b\}$
125		eqid	$⊢ (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)) = (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c))$
126	125	rnmpt	$⊢ ran (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)) = \{u \| \exists z \in a u = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)\}$
127	122 124 126	3eqtr4g	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to ran (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b) = ran (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c))$
128	39	ad2antrr	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to \underset{˙}{\oplus} : X \times (P pSyl G) ⟶ P pSyl G$
129	128 79 80	fovcdmd	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to c \underset{˙}{\oplus} a \in (P pSyl G)$
130		simpr	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to y = c \underset{˙}{\oplus} a$
131		simpl	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to x = b$
132	131	oveq1d	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to x \underset{˙}{+} z = b \underset{˙}{+} z$
133	132 131	oveq12d	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to (x \underset{˙}{+} z) \underset{˙}{-} x = (b \underset{˙}{+} z) \underset{˙}{-} b$
134	130 133	mpteq12dv	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} z) \underset{˙}{-} b)$
135		oveq2	$⊢ z = w \to b \underset{˙}{+} z = b \underset{˙}{+} w$
136	135	oveq1d	$⊢ z = w \to (b \underset{˙}{+} z) \underset{˙}{-} b = (b \underset{˙}{+} w) \underset{˙}{-} b$
137	136	cbvmptv	$⊢ (z \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} z) \underset{˙}{-} b) = (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b)$
138	134 137	eqtrdi	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b)$
139	138	rneqd	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = ran (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b)$
140		ovex	$⊢ c \underset{˙}{\oplus} a \in V$
141	140	mptex	$⊢ (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b) \in V$
142	141	rnex	$⊢ ran (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b) \in V$
143	139 7 142	ovmpoa	$⊢ (b \in X \land c \underset{˙}{\oplus} a \in (P pSyl G)) \to b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a) = ran (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b)$
144	98 129 143	syl2anc	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a) = ran (w \in (c \underset{˙}{\oplus} a) ⟼ (b \underset{˙}{+} w) \underset{˙}{-} b)$
145		simpr	$⊢ (x = b \underset{˙}{+} c \land y = a) \to y = a$
146		simpl	$⊢ (x = b \underset{˙}{+} c \land y = a) \to x = b \underset{˙}{+} c$
147	146	oveq1d	$⊢ (x = b \underset{˙}{+} c \land y = a) \to x \underset{˙}{+} z = (b \underset{˙}{+} c) \underset{˙}{+} z$
148	147 146	oveq12d	$⊢ (x = b \underset{˙}{+} c \land y = a) \to (x \underset{˙}{+} z) \underset{˙}{-} x = ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)$
149	145 148	mpteq12dv	$⊢ (x = b \underset{˙}{+} c \land y = a) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c))$
150	149	rneqd	$⊢ (x = b \underset{˙}{+} c \land y = a) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = ran (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c))$
151	51	mptex	$⊢ (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)) \in V$
152	151	rnex	$⊢ ran (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c)) \in V$
153	150 7 152	ovmpoa	$⊢ (b \underset{˙}{+} c \in X \land a \in (P pSyl G)) \to (b \underset{˙}{+} c) \underset{˙}{\oplus} a = ran (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c))$
154	100 80 153	syl2anc	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to (b \underset{˙}{+} c) \underset{˙}{\oplus} a = ran (z \in a ⟼ ((b \underset{˙}{+} c) \underset{˙}{+} z) \underset{˙}{-} (b \underset{˙}{+} c))$
155	127 144 154	3eqtr4rd	$⊢ ((φ \land a \in (P pSyl G)) \land (b \in X \land c \in X)) \to (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a)$
156	155	ralrimivva	$⊢ (φ \land a \in (P pSyl G)) \to \forall b \in X \forall c \in X (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a)$
157	74 156	jca	$⊢ (φ \land a \in (P pSyl G)) \to (0_{G} \underset{˙}{\oplus} a = a \land \forall b \in X \forall c \in X (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a))$
158	157	ralrimiva	$⊢ φ \to \forall a \in (P pSyl G) (0_{G} \underset{˙}{\oplus} a = a \land \forall b \in X \forall c \in X (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a))$
159	39 158	jca	$⊢ φ \to (\underset{˙}{\oplus} : X \times (P pSyl G) ⟶ P pSyl G \land \forall a \in (P pSyl G) (0_{G} \underset{˙}{\oplus} a = a \land \forall b \in X \forall c \in X (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a)))$
160	1 5 41	isga	$⊢ \underset{˙}{\oplus} \in (G GrpAct (P pSyl G)) \leftrightarrow ((G \in Grp \land P pSyl G \in V) \land (\underset{˙}{\oplus} : X \times (P pSyl G) ⟶ P pSyl G \land \forall a \in (P pSyl G) (0_{G} \underset{˙}{\oplus} a = a \land \forall b \in X \forall c \in X (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a))))$
161	9 159 160	sylanbrc	$⊢ φ \to \underset{˙}{\oplus} \in (G GrpAct (P pSyl G))$

Metamath Proof Explorer

Theorem sylow3lem1

Proof