sylow1lem2

Description: Lemma for sylow1 . The function .(+) is a group action on S . (Contributed by Mario Carneiro, 15-Jan-2015)

	Ref	Expression
Hypotheses	sylow1.x	$⊢ X = {Base}_{G}$
	sylow1.g	$⊢ φ \to G \in Grp$
	sylow1.f	$⊢ φ \to X \in Fin$
	sylow1.p	$⊢ φ \to P \in ℙ$
	sylow1.n	$⊢ φ \to N \in ℕ_{0}$
	sylow1.d	$⊢ φ \to P^{N} ∥ \|X\|$
	sylow1lem.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow1lem.s	$⊢ S = \{s \in 𝒫 X \| \|s\| = P^{N}\}$
	sylow1lem.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in S ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
Assertion	sylow1lem2	$⊢ φ \to \underset{˙}{\oplus} \in (G GrpAct S)$

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	$⊢ X = {Base}_{G}$
2		sylow1.g	$⊢ φ \to G \in Grp$
3		sylow1.f	$⊢ φ \to X \in Fin$
4		sylow1.p	$⊢ φ \to P \in ℙ$
5		sylow1.n	$⊢ φ \to N \in ℕ_{0}$
6		sylow1.d	$⊢ φ \to P^{N} ∥ \|X\|$
7		sylow1lem.a	$⊢ \underset{˙}{+} = +_{G}$
8		sylow1lem.s	$⊢ S = \{s \in 𝒫 X \| \|s\| = P^{N}\}$
9		sylow1lem.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in S ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
10	1	fvexi	$⊢ X \in V$
11	10	pwex	$⊢ 𝒫 X \in V$
12	8 11	rabex2	$⊢ S \in V$
13	2 12	jctir	$⊢ φ \to (G \in Grp \land S \in V)$
14		simprl	$⊢ (φ \land (x \in X \land y \in S)) \to x \in X$
15		eqid	$⊢ (z \in X ⟼ x \underset{˙}{+} z) = (z \in X ⟼ x \underset{˙}{+} z)$
16	1 7 15	grplmulf1o	$⊢ (G \in Grp \land x \in X) \to (z \in X ⟼ x \underset{˙}{+} z) : X \underset{1-1 onto}{⟶} X$
17	2 14 16	syl2an2r	$⊢ (φ \land (x \in X \land y \in S)) \to (z \in X ⟼ x \underset{˙}{+} z) : X \underset{1-1 onto}{⟶} X$
18		f1of1	$⊢ (z \in X ⟼ x \underset{˙}{+} z) : X \underset{1-1 onto}{⟶} X \to (z \in X ⟼ x \underset{˙}{+} z) : X \underset{1-1}{⟶} X$
19	17 18	syl	$⊢ (φ \land (x \in X \land y \in S)) \to (z \in X ⟼ x \underset{˙}{+} z) : X \underset{1-1}{⟶} X$
20		simprr	$⊢ (φ \land (x \in X \land y \in S)) \to y \in S$
21		fveqeq2	$⊢ s = y \to (\|s\| = P^{N} \leftrightarrow \|y\| = P^{N})$
22	21 8	elrab2	$⊢ y \in S \leftrightarrow (y \in 𝒫 X \land \|y\| = P^{N})$
23	20 22	sylib	$⊢ (φ \land (x \in X \land y \in S)) \to (y \in 𝒫 X \land \|y\| = P^{N})$
24	23	simpld	$⊢ (φ \land (x \in X \land y \in S)) \to y \in 𝒫 X$
25	24	elpwid	$⊢ (φ \land (x \in X \land y \in S)) \to y \subseteq X$
26		f1ssres	$⊢ ((z \in X ⟼ x \underset{˙}{+} z) : X \underset{1-1}{⟶} X \land y \subseteq X) \to ({(z \in X ⟼ x \underset{˙}{+} z) ↾}_{y}) : y \underset{1-1}{⟶} X$
27	19 25 26	syl2anc	$⊢ (φ \land (x \in X \land y \in S)) \to ({(z \in X ⟼ x \underset{˙}{+} z) ↾}_{y}) : y \underset{1-1}{⟶} X$
28		resmpt	$⊢ y \subseteq X \to {(z \in X ⟼ x \underset{˙}{+} z) ↾}_{y} = (z \in y ⟼ x \underset{˙}{+} z)$
29		f1eq1	$⊢ {(z \in X ⟼ x \underset{˙}{+} z) ↾}_{y} = (z \in y ⟼ x \underset{˙}{+} z) \to (({(z \in X ⟼ x \underset{˙}{+} z) ↾}_{y}) : y \underset{1-1}{⟶} X \leftrightarrow (z \in y ⟼ x \underset{˙}{+} z) : y \underset{1-1}{⟶} X)$
30	25 28 29	3syl	$⊢ (φ \land (x \in X \land y \in S)) \to (({(z \in X ⟼ x \underset{˙}{+} z) ↾}_{y}) : y \underset{1-1}{⟶} X \leftrightarrow (z \in y ⟼ x \underset{˙}{+} z) : y \underset{1-1}{⟶} X)$
31	27 30	mpbid	$⊢ (φ \land (x \in X \land y \in S)) \to (z \in y ⟼ x \underset{˙}{+} z) : y \underset{1-1}{⟶} X$
32		f1f	$⊢ (z \in y ⟼ x \underset{˙}{+} z) : y \underset{1-1}{⟶} X \to (z \in y ⟼ x \underset{˙}{+} z) : y ⟶ X$
33		frn	$⊢ (z \in y ⟼ x \underset{˙}{+} z) : y ⟶ X \to ran (z \in y ⟼ x \underset{˙}{+} z) \subseteq X$
34	31 32 33	3syl	$⊢ (φ \land (x \in X \land y \in S)) \to ran (z \in y ⟼ x \underset{˙}{+} z) \subseteq X$
35	10	elpw2	$⊢ ran (z \in y ⟼ x \underset{˙}{+} z) \in 𝒫 X \leftrightarrow ran (z \in y ⟼ x \underset{˙}{+} z) \subseteq X$
36	34 35	sylibr	$⊢ (φ \land (x \in X \land y \in S)) \to ran (z \in y ⟼ x \underset{˙}{+} z) \in 𝒫 X$
37		f1f1orn	$⊢ (z \in y ⟼ x \underset{˙}{+} z) : y \underset{1-1}{⟶} X \to (z \in y ⟼ x \underset{˙}{+} z) : y \underset{1-1 onto}{⟶} ran (z \in y ⟼ x \underset{˙}{+} z)$
38		vex	$⊢ y \in V$
39	38	f1oen	$⊢ (z \in y ⟼ x \underset{˙}{+} z) : y \underset{1-1 onto}{⟶} ran (z \in y ⟼ x \underset{˙}{+} z) \to y \approx ran (z \in y ⟼ x \underset{˙}{+} z)$
40	31 37 39	3syl	$⊢ (φ \land (x \in X \land y \in S)) \to y \approx ran (z \in y ⟼ x \underset{˙}{+} z)$
41		ssfi	$⊢ (X \in Fin \land y \subseteq X) \to y \in Fin$
42	3 25 41	syl2an2r	$⊢ (φ \land (x \in X \land y \in S)) \to y \in Fin$
43		ssfi	$⊢ (X \in Fin \land ran (z \in y ⟼ x \underset{˙}{+} z) \subseteq X) \to ran (z \in y ⟼ x \underset{˙}{+} z) \in Fin$
44	3 34 43	syl2an2r	$⊢ (φ \land (x \in X \land y \in S)) \to ran (z \in y ⟼ x \underset{˙}{+} z) \in Fin$
45		hashen	$⊢ (y \in Fin \land ran (z \in y ⟼ x \underset{˙}{+} z) \in Fin) \to (\|y\| = \|ran (z \in y ⟼ x \underset{˙}{+} z)\| \leftrightarrow y \approx ran (z \in y ⟼ x \underset{˙}{+} z))$
46	42 44 45	syl2anc	$⊢ (φ \land (x \in X \land y \in S)) \to (\|y\| = \|ran (z \in y ⟼ x \underset{˙}{+} z)\| \leftrightarrow y \approx ran (z \in y ⟼ x \underset{˙}{+} z))$
47	40 46	mpbird	$⊢ (φ \land (x \in X \land y \in S)) \to \|y\| = \|ran (z \in y ⟼ x \underset{˙}{+} z)\|$
48	23	simprd	$⊢ (φ \land (x \in X \land y \in S)) \to \|y\| = P^{N}$
49	47 48	eqtr3d	$⊢ (φ \land (x \in X \land y \in S)) \to \|ran (z \in y ⟼ x \underset{˙}{+} z)\| = P^{N}$
50		fveqeq2	$⊢ s = ran (z \in y ⟼ x \underset{˙}{+} z) \to (\|s\| = P^{N} \leftrightarrow \|ran (z \in y ⟼ x \underset{˙}{+} z)\| = P^{N})$
51	50 8	elrab2	$⊢ ran (z \in y ⟼ x \underset{˙}{+} z) \in S \leftrightarrow (ran (z \in y ⟼ x \underset{˙}{+} z) \in 𝒫 X \land \|ran (z \in y ⟼ x \underset{˙}{+} z)\| = P^{N})$
52	36 49 51	sylanbrc	$⊢ (φ \land (x \in X \land y \in S)) \to ran (z \in y ⟼ x \underset{˙}{+} z) \in S$
53	52	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in S ran (z \in y ⟼ x \underset{˙}{+} z) \in S$
54	9	fmpo	$⊢ \forall x \in X \forall y \in S ran (z \in y ⟼ x \underset{˙}{+} z) \in S \leftrightarrow \underset{˙}{\oplus} : X \times S ⟶ S$
55	53 54	sylib	$⊢ φ \to \underset{˙}{\oplus} : X \times S ⟶ S$
56	2	adantr	$⊢ (φ \land a \in S) \to G \in Grp$
57		eqid	$⊢ 0_{G} = 0_{G}$
58	1 57	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
59	56 58	syl	$⊢ (φ \land a \in S) \to 0_{G} \in X$
60		simpr	$⊢ (φ \land a \in S) \to a \in S$
61		simpr	$⊢ (x = 0_{G} \land y = a) \to y = a$
62		simpl	$⊢ (x = 0_{G} \land y = a) \to x = 0_{G}$
63	62	oveq1d	$⊢ (x = 0_{G} \land y = a) \to x \underset{˙}{+} z = 0_{G} \underset{˙}{+} z$
64	61 63	mpteq12dv	$⊢ (x = 0_{G} \land y = a) \to (z \in y ⟼ x \underset{˙}{+} z) = (z \in a ⟼ 0_{G} \underset{˙}{+} z)$
65	64	rneqd	$⊢ (x = 0_{G} \land y = a) \to ran (z \in y ⟼ x \underset{˙}{+} z) = ran (z \in a ⟼ 0_{G} \underset{˙}{+} z)$
66		vex	$⊢ a \in V$
67	66	mptex	$⊢ (z \in a ⟼ 0_{G} \underset{˙}{+} z) \in V$
68	67	rnex	$⊢ ran (z \in a ⟼ 0_{G} \underset{˙}{+} z) \in V$
69	65 9 68	ovmpoa	$⊢ (0_{G} \in X \land a \in S) \to 0_{G} \underset{˙}{\oplus} a = ran (z \in a ⟼ 0_{G} \underset{˙}{+} z)$
70	59 60 69	syl2anc	$⊢ (φ \land a \in S) \to 0_{G} \underset{˙}{\oplus} a = ran (z \in a ⟼ 0_{G} \underset{˙}{+} z)$
71	8	ssrab3	$⊢ S \subseteq 𝒫 X$
72	71 60	sselid	$⊢ (φ \land a \in S) \to a \in 𝒫 X$
73	72	elpwid	$⊢ (φ \land a \in S) \to a \subseteq X$
74	73	sselda	$⊢ ((φ \land a \in S) \land z \in a) \to z \in X$
75	1 7 57	grplid	$⊢ (G \in Grp \land z \in X) \to 0_{G} \underset{˙}{+} z = z$
76	56 74 75	syl2an2r	$⊢ ((φ \land a \in S) \land z \in a) \to 0_{G} \underset{˙}{+} z = z$
77	76	mpteq2dva	$⊢ (φ \land a \in S) \to (z \in a ⟼ 0_{G} \underset{˙}{+} z) = (z \in a ⟼ z)$
78		mptresid	$⊢ {I ↾}_{a} = (z \in a ⟼ z)$
79	77 78	eqtr4di	$⊢ (φ \land a \in S) \to (z \in a ⟼ 0_{G} \underset{˙}{+} z) = {I ↾}_{a}$
80	79	rneqd	$⊢ (φ \land a \in S) \to ran (z \in a ⟼ 0_{G} \underset{˙}{+} z) = ran ({I ↾}_{a})$
81		rnresi	$⊢ ran ({I ↾}_{a}) = a$
82	80 81	eqtrdi	$⊢ (φ \land a \in S) \to ran (z \in a ⟼ 0_{G} \underset{˙}{+} z) = a$
83	70 82	eqtrd	$⊢ (φ \land a \in S) \to 0_{G} \underset{˙}{\oplus} a = a$
84		ovex	$⊢ c \underset{˙}{+} z \in V$
85		oveq2	$⊢ w = c \underset{˙}{+} z \to b \underset{˙}{+} w = b \underset{˙}{+} (c \underset{˙}{+} z)$
86	84 85	abrexco	$⊢ \{u \| \exists w \in \{v \| \exists z \in a v = c \underset{˙}{+} z\} u = b \underset{˙}{+} w\} = \{u \| \exists z \in a u = b \underset{˙}{+} (c \underset{˙}{+} z)\}$
87		simprr	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to c \in X$
88	60	adantr	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to a \in S$
89		simpr	$⊢ (x = c \land y = a) \to y = a$
90		simpl	$⊢ (x = c \land y = a) \to x = c$
91	90	oveq1d	$⊢ (x = c \land y = a) \to x \underset{˙}{+} z = c \underset{˙}{+} z$
92	89 91	mpteq12dv	$⊢ (x = c \land y = a) \to (z \in y ⟼ x \underset{˙}{+} z) = (z \in a ⟼ c \underset{˙}{+} z)$
93	92	rneqd	$⊢ (x = c \land y = a) \to ran (z \in y ⟼ x \underset{˙}{+} z) = ran (z \in a ⟼ c \underset{˙}{+} z)$
94	66	mptex	$⊢ (z \in a ⟼ c \underset{˙}{+} z) \in V$
95	94	rnex	$⊢ ran (z \in a ⟼ c \underset{˙}{+} z) \in V$
96	93 9 95	ovmpoa	$⊢ (c \in X \land a \in S) \to c \underset{˙}{\oplus} a = ran (z \in a ⟼ c \underset{˙}{+} z)$
97	87 88 96	syl2anc	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to c \underset{˙}{\oplus} a = ran (z \in a ⟼ c \underset{˙}{+} z)$
98		eqid	$⊢ (z \in a ⟼ c \underset{˙}{+} z) = (z \in a ⟼ c \underset{˙}{+} z)$
99	98	rnmpt	$⊢ ran (z \in a ⟼ c \underset{˙}{+} z) = \{v \| \exists z \in a v = c \underset{˙}{+} z\}$
100	97 99	eqtrdi	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to c \underset{˙}{\oplus} a = \{v \| \exists z \in a v = c \underset{˙}{+} z\}$
101	100	rexeqdv	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to (\exists w \in (c \underset{˙}{\oplus} a) u = b \underset{˙}{+} w \leftrightarrow \exists w \in \{v \| \exists z \in a v = c \underset{˙}{+} z\} u = b \underset{˙}{+} w)$
102	101	abbidv	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to \{u \| \exists w \in (c \underset{˙}{\oplus} a) u = b \underset{˙}{+} w\} = \{u \| \exists w \in \{v \| \exists z \in a v = c \underset{˙}{+} z\} u = b \underset{˙}{+} w\}$
103	56	ad2antrr	$⊢ (((φ \land a \in S) \land (b \in X \land c \in X)) \land z \in a) \to G \in Grp$
104		simprl	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to b \in X$
105	104	adantr	$⊢ (((φ \land a \in S) \land (b \in X \land c \in X)) \land z \in a) \to b \in X$
106	87	adantr	$⊢ (((φ \land a \in S) \land (b \in X \land c \in X)) \land z \in a) \to c \in X$
107	74	adantlr	$⊢ (((φ \land a \in S) \land (b \in X \land c \in X)) \land z \in a) \to z \in X$
108	1 7	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)$
109	103 105 106 107 108	syl13anc	$⊢ (((φ \land a \in S) \land (b \in X \land c \in X)) \land z \in a) \to (b \underset{˙}{+} c) \underset{˙}{+} z = b \underset{˙}{+} (c \underset{˙}{+} z)$
110	109	eqeq2d	$⊢ (((φ \land a \in S) \land (b \in X \land c \in X)) \land z \in a) \to (u = (b \underset{˙}{+} c) \underset{˙}{+} z \leftrightarrow u = b \underset{˙}{+} (c \underset{˙}{+} z))$
111	110	rexbidva	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to (\exists z \in a u = (b \underset{˙}{+} c) \underset{˙}{+} z \leftrightarrow \exists z \in a u = b \underset{˙}{+} (c \underset{˙}{+} z))$
112	111	abbidv	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to \{u \| \exists z \in a u = (b \underset{˙}{+} c) \underset{˙}{+} z\} = \{u \| \exists z \in a u = b \underset{˙}{+} (c \underset{˙}{+} z)\}$
113	86 102 112	3eqtr4a	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to \{u \| \exists w \in (c \underset{˙}{\oplus} a) u = b \underset{˙}{+} w\} = \{u \| \exists z \in a u = (b \underset{˙}{+} c) \underset{˙}{+} z\}$
114		eqid	$⊢ (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w) = (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w)$
115	114	rnmpt	$⊢ ran (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w) = \{u \| \exists w \in (c \underset{˙}{\oplus} a) u = b \underset{˙}{+} w\}$
116		eqid	$⊢ (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z) = (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z)$
117	116	rnmpt	$⊢ ran (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z) = \{u \| \exists z \in a u = (b \underset{˙}{+} c) \underset{˙}{+} z\}$
118	113 115 117	3eqtr4g	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to ran (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w) = ran (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z)$
119	55	ad2antrr	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to \underset{˙}{\oplus} : X \times S ⟶ S$
120	119 87 88	fovcdmd	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to c \underset{˙}{\oplus} a \in S$
121		simpr	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to y = c \underset{˙}{\oplus} a$
122		simpl	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to x = b$
123	122	oveq1d	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to x \underset{˙}{+} z = b \underset{˙}{+} z$
124	121 123	mpteq12dv	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to (z \in y ⟼ x \underset{˙}{+} z) = (z \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} z)$
125		oveq2	$⊢ z = w \to b \underset{˙}{+} z = b \underset{˙}{+} w$
126	125	cbvmptv	$⊢ (z \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} z) = (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w)$
127	124 126	eqtrdi	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to (z \in y ⟼ x \underset{˙}{+} z) = (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w)$
128	127	rneqd	$⊢ (x = b \land y = c \underset{˙}{\oplus} a) \to ran (z \in y ⟼ x \underset{˙}{+} z) = ran (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w)$
129		ovex	$⊢ c \underset{˙}{\oplus} a \in V$
130	129	mptex	$⊢ (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w) \in V$
131	130	rnex	$⊢ ran (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w) \in V$
132	128 9 131	ovmpoa	$⊢ (b \in X \land c \underset{˙}{\oplus} a \in S) \to b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a) = ran (w \in (c \underset{˙}{\oplus} a) ⟼ b \underset{˙}{+} w)$
133	104 120 132	syl2anc	$⊢ ((φ \land a \in S) \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)$
134	2	ad2antrr	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to G \in Grp$
135	1 7	grpcl	$⊢ (G \in Grp \land b \in X \land c \in X) \to b \underset{˙}{+} c \in X$
136	134 104 87 135	syl3anc	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to b \underset{˙}{+} c \in X$
137		simpr	$⊢ (x = b \underset{˙}{+} c \land y = a) \to y = a$
138		simpl	$⊢ (x = b \underset{˙}{+} c \land y = a) \to x = b \underset{˙}{+} c$
139	138	oveq1d	$⊢ (x = b \underset{˙}{+} c \land y = a) \to x \underset{˙}{+} z = (b \underset{˙}{+} c) \underset{˙}{+} z$
140	137 139	mpteq12dv	$⊢ (x = b \underset{˙}{+} c \land y = a) \to (z \in y ⟼ x \underset{˙}{+} z) = (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z)$
141	140	rneqd	$⊢ (x = b \underset{˙}{+} c \land y = a) \to ran (z \in y ⟼ x \underset{˙}{+} z) = ran (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z)$
142	66	mptex	$⊢ (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z) \in V$
143	142	rnex	$⊢ ran (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z) \in V$
144	141 9 143	ovmpoa	$⊢ (b \underset{˙}{+} c \in X \land a \in S) \to (b \underset{˙}{+} c) \underset{˙}{\oplus} a = ran (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z)$
145	136 88 144	syl2anc	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to (b \underset{˙}{+} c) \underset{˙}{\oplus} a = ran (z \in a ⟼ (b \underset{˙}{+} c) \underset{˙}{+} z)$
146	118 133 145	3eqtr4rd	$⊢ ((φ \land a \in S) \land (b \in X \land c \in X)) \to (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a)$
147	146	ralrimivva	$⊢ (φ \land a \in S) \to \forall b \in X \forall c \in X (b \underset{˙}{+} c) \underset{˙}{\oplus} a = b \underset{˙}{\oplus} (c \underset{˙}{\oplus} a)$
148	83 147	jca	$⊢ (φ \land a \in S) \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))$
149	148	ralrimiva	$⊢ φ \to \forall a \in S (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))$
150	55 149	jca	$⊢ φ \to (\underset{˙}{\oplus} : X \times S ⟶ S \land \forall a \in S (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)))$
151	1 7 57	isga	$⊢ \underset{˙}{\oplus} \in (G GrpAct S) \leftrightarrow ((G \in Grp \land S \in V) \land (\underset{˙}{\oplus} : X \times S ⟶ S \land \forall a \in S (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))))$
152	13 150 151	sylanbrc	$⊢ φ \to \underset{˙}{\oplus} \in (G GrpAct S)$

Metamath Proof Explorer

Theorem sylow1lem2

Proof