Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
	sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
	sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
	sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
Assertion	sylow1lem2	⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
7		sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
8		sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
9		sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
10	1	fvexi	⊢ 𝑋 ∈ V
11	10	pwex	⊢ 𝒫 𝑋 ∈ V
12	8 11	rabex2	⊢ 𝑆 ∈ V
13	2 12	jctir	⊢ ( 𝜑 → ( 𝐺 ∈ Grp ∧ 𝑆 ∈ V ) )
14		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ 𝑋 )
15		eqid	⊢ ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) )
16	1 7 15	grplmulf1o	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
17	2 14 16	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
18		f1of1	⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) : 𝑋 –1-1→ 𝑋 )
19	17 18	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) : 𝑋 –1-1→ 𝑋 )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
21		fveqeq2	⊢ ( 𝑠 = 𝑦 → ( ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) ↔ ( ♯ ‘ 𝑦 ) = ( 𝑃 ↑ 𝑁 ) ) )
22	21 8	elrab2	⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑃 ↑ 𝑁 ) ) )
23	20 22	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑦 ∈ 𝒫 𝑋 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑃 ↑ 𝑁 ) ) )
24	23	simpld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝒫 𝑋 )
25	24	elpwid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ⊆ 𝑋 )
26		f1ssres	⊢ ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) : 𝑋 –1-1→ 𝑋 ∧ 𝑦 ⊆ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) ↾ 𝑦 ) : 𝑦 –1-1→ 𝑋 )
27	19 25 26	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) ↾ 𝑦 ) : 𝑦 –1-1→ 𝑋 )
28		resmpt	⊢ ( 𝑦 ⊆ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) ↾ 𝑦 ) = ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
29		f1eq1	⊢ ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) ↾ 𝑦 ) = ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) ↾ 𝑦 ) : 𝑦 –1-1→ 𝑋 ↔ ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 –1-1→ 𝑋 ) )
30	25 28 29	3syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 + 𝑧 ) ) ↾ 𝑦 ) : 𝑦 –1-1→ 𝑋 ↔ ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 –1-1→ 𝑋 ) )
31	27 30	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 –1-1→ 𝑋 )
32		f1f	⊢ ( ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 –1-1→ 𝑋 → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 ⟶ 𝑋 )
33		frn	⊢ ( ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 ⟶ 𝑋 → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ⊆ 𝑋 )
34	31 32 33	3syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ⊆ 𝑋 )
35	10	elpw2	⊢ ( ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ 𝒫 𝑋 ↔ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ⊆ 𝑋 )
36	34 35	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ 𝒫 𝑋 )
37		f1f1orn	⊢ ( ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 –1-1→ 𝑋 → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 –1-1-onto→ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
38		vex	⊢ 𝑦 ∈ V
39	38	f1oen	⊢ ( ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) : 𝑦 –1-1-onto→ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) → 𝑦 ≈ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
40	31 37 39	3syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ≈ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
41		ssfi	⊢ ( ( 𝑋 ∈ Fin ∧ 𝑦 ⊆ 𝑋 ) → 𝑦 ∈ Fin )
42	3 25 41	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ Fin )
43		ssfi	⊢ ( ( 𝑋 ∈ Fin ∧ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ⊆ 𝑋 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ Fin )
44	3 34 43	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ Fin )
45		hashen	⊢ ( ( 𝑦 ∈ Fin ∧ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) ↔ 𝑦 ≈ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) )
46	42 44 45	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) ↔ 𝑦 ≈ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) )
47	40 46	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) )
48	23	simprd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( ♯ ‘ 𝑦 ) = ( 𝑃 ↑ 𝑁 ) )
49	47 48	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( ♯ ‘ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) = ( 𝑃 ↑ 𝑁 ) )
50		fveqeq2	⊢ ( 𝑠 = ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) → ( ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) ↔ ( ♯ ‘ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) = ( 𝑃 ↑ 𝑁 ) ) )
51	50 8	elrab2	⊢ ( ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ 𝑆 ↔ ( ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ 𝒫 𝑋 ∧ ( ♯ ‘ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ) = ( 𝑃 ↑ 𝑁 ) ) )
52	36 49 51	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ 𝑆 )
53	52	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ 𝑆 )
54	9	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ 𝑆 ↔ ⊕ : ( 𝑋 × 𝑆 ) ⟶ 𝑆 )
55	53 54	sylib	⊢ ( 𝜑 → ⊕ : ( 𝑋 × 𝑆 ) ⟶ 𝑆 )
56	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐺 ∈ Grp )
57		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
58	1 57	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
59	56 58	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
60		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 )
61		simpr	⊢ ( ( 𝑥 = ( 0g ‘ 𝐺 ) ∧ 𝑦 = 𝑎 ) → 𝑦 = 𝑎 )
62		simpl	⊢ ( ( 𝑥 = ( 0g ‘ 𝐺 ) ∧ 𝑦 = 𝑎 ) → 𝑥 = ( 0g ‘ 𝐺 ) )
63	62	oveq1d	⊢ ( ( 𝑥 = ( 0g ‘ 𝐺 ) ∧ 𝑦 = 𝑎 ) → ( 𝑥 + 𝑧 ) = ( ( 0g ‘ 𝐺 ) + 𝑧 ) )
64	61 63	mpteq12dv	⊢ ( ( 𝑥 = ( 0g ‘ 𝐺 ) ∧ 𝑦 = 𝑎 ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) )
65	64	rneqd	⊢ ( ( 𝑥 = ( 0g ‘ 𝐺 ) ∧ 𝑦 = 𝑎 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ran ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) )
66		vex	⊢ 𝑎 ∈ V
67	66	mptex	⊢ ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) ∈ V
68	67	rnex	⊢ ran ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) ∈ V
69	65 9 68	ovmpoa	⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑋 ∧ 𝑎 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝑎 ) = ran ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) )
70	59 60 69	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝑎 ) = ran ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) )
71	8	ssrab3	⊢ 𝑆 ⊆ 𝒫 𝑋
72	71 60	sselid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝒫 𝑋 )
73	72	elpwid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ⊆ 𝑋 )
74	73	sselda	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑎 ) → 𝑧 ∈ 𝑋 )
75	1 7 57	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑧 ) = 𝑧 )
76	56 74 75	syl2an2r	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑎 ) → ( ( 0g ‘ 𝐺 ) + 𝑧 ) = 𝑧 )
77	76	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) = ( 𝑧 ∈ 𝑎 ↦ 𝑧 ) )
78		mptresid	⊢ ( I ↾ 𝑎 ) = ( 𝑧 ∈ 𝑎 ↦ 𝑧 )
79	77 78	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) = ( I ↾ 𝑎 ) )
80	79	rneqd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ran ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) = ran ( I ↾ 𝑎 ) )
81		rnresi	⊢ ran ( I ↾ 𝑎 ) = 𝑎
82	80 81	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ran ( 𝑧 ∈ 𝑎 ↦ ( ( 0g ‘ 𝐺 ) + 𝑧 ) ) = 𝑎 )
83	70 82	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝑎 ) = 𝑎 )
84		ovex	⊢ ( 𝑐 + 𝑧 ) ∈ V
85		oveq2	⊢ ( 𝑤 = ( 𝑐 + 𝑧 ) → ( 𝑏 + 𝑤 ) = ( 𝑏 + ( 𝑐 + 𝑧 ) ) )
86	84 85	abrexco	⊢ { 𝑢 ∣ ∃ 𝑤 ∈ { 𝑣 ∣ ∃ 𝑧 ∈ 𝑎 𝑣 = ( 𝑐 + 𝑧 ) } 𝑢 = ( 𝑏 + 𝑤 ) } = { 𝑢 ∣ ∃ 𝑧 ∈ 𝑎 𝑢 = ( 𝑏 + ( 𝑐 + 𝑧 ) ) }
87		simprr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝑐 ∈ 𝑋 )
88	60	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑆 )
89		simpr	⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑎 ) → 𝑦 = 𝑎 )
90		simpl	⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑎 ) → 𝑥 = 𝑐 )
91	90	oveq1d	⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑎 ) → ( 𝑥 + 𝑧 ) = ( 𝑐 + 𝑧 ) )
92	89 91	mpteq12dv	⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑎 ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) )
93	92	rneqd	⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑎 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ran ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) )
94	66	mptex	⊢ ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) ∈ V
95	94	rnex	⊢ ran ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) ∈ V
96	93 9 95	ovmpoa	⊢ ( ( 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑐 ⊕ 𝑎 ) = ran ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) )
97	87 88 96	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 ⊕ 𝑎 ) = ran ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) )
98		eqid	⊢ ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) = ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) )
99	98	rnmpt	⊢ ran ( 𝑧 ∈ 𝑎 ↦ ( 𝑐 + 𝑧 ) ) = { 𝑣 ∣ ∃ 𝑧 ∈ 𝑎 𝑣 = ( 𝑐 + 𝑧 ) }
100	97 99	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 ⊕ 𝑎 ) = { 𝑣 ∣ ∃ 𝑧 ∈ 𝑎 𝑣 = ( 𝑐 + 𝑧 ) } )
101	100	rexeqdv	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( ∃ 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) 𝑢 = ( 𝑏 + 𝑤 ) ↔ ∃ 𝑤 ∈ { 𝑣 ∣ ∃ 𝑧 ∈ 𝑎 𝑣 = ( 𝑐 + 𝑧 ) } 𝑢 = ( 𝑏 + 𝑤 ) ) )
102	101	abbidv	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → { 𝑢 ∣ ∃ 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) 𝑢 = ( 𝑏 + 𝑤 ) } = { 𝑢 ∣ ∃ 𝑤 ∈ { 𝑣 ∣ ∃ 𝑧 ∈ 𝑎 𝑣 = ( 𝑐 + 𝑧 ) } 𝑢 = ( 𝑏 + 𝑤 ) } )
103	56	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑎 ) → 𝐺 ∈ Grp )
104		simprl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝑏 ∈ 𝑋 )
105	104	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑎 ) → 𝑏 ∈ 𝑋 )
106	87	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑎 ) → 𝑐 ∈ 𝑋 )
107	74	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑎 ) → 𝑧 ∈ 𝑋 )
108	1 7	grpass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑏 + 𝑐 ) + 𝑧 ) = ( 𝑏 + ( 𝑐 + 𝑧 ) ) )
109	103 105 106 107 108	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑎 ) → ( ( 𝑏 + 𝑐 ) + 𝑧 ) = ( 𝑏 + ( 𝑐 + 𝑧 ) ) )
110	109	eqeq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑎 ) → ( 𝑢 = ( ( 𝑏 + 𝑐 ) + 𝑧 ) ↔ 𝑢 = ( 𝑏 + ( 𝑐 + 𝑧 ) ) ) )
111	110	rexbidva	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( ∃ 𝑧 ∈ 𝑎 𝑢 = ( ( 𝑏 + 𝑐 ) + 𝑧 ) ↔ ∃ 𝑧 ∈ 𝑎 𝑢 = ( 𝑏 + ( 𝑐 + 𝑧 ) ) ) )
112	111	abbidv	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → { 𝑢 ∣ ∃ 𝑧 ∈ 𝑎 𝑢 = ( ( 𝑏 + 𝑐 ) + 𝑧 ) } = { 𝑢 ∣ ∃ 𝑧 ∈ 𝑎 𝑢 = ( 𝑏 + ( 𝑐 + 𝑧 ) ) } )
113	86 102 112	3eqtr4a	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → { 𝑢 ∣ ∃ 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) 𝑢 = ( 𝑏 + 𝑤 ) } = { 𝑢 ∣ ∃ 𝑧 ∈ 𝑎 𝑢 = ( ( 𝑏 + 𝑐 ) + 𝑧 ) } )
114		eqid	⊢ ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) = ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) )
115	114	rnmpt	⊢ ran ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) = { 𝑢 ∣ ∃ 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) 𝑢 = ( 𝑏 + 𝑤 ) }
116		eqid	⊢ ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) = ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) )
117	116	rnmpt	⊢ ran ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) = { 𝑢 ∣ ∃ 𝑧 ∈ 𝑎 𝑢 = ( ( 𝑏 + 𝑐 ) + 𝑧 ) }
118	113 115 117	3eqtr4g	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ran ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) = ran ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) )
119	55	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ⊕ : ( 𝑋 × 𝑆 ) ⟶ 𝑆 )
120	119 87 88	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 ⊕ 𝑎 ) ∈ 𝑆 )
121		simpr	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = ( 𝑐 ⊕ 𝑎 ) ) → 𝑦 = ( 𝑐 ⊕ 𝑎 ) )
122		simpl	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = ( 𝑐 ⊕ 𝑎 ) ) → 𝑥 = 𝑏 )
123	122	oveq1d	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = ( 𝑐 ⊕ 𝑎 ) ) → ( 𝑥 + 𝑧 ) = ( 𝑏 + 𝑧 ) )
124	121 123	mpteq12dv	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = ( 𝑐 ⊕ 𝑎 ) ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑧 ) ) )
125		oveq2	⊢ ( 𝑧 = 𝑤 → ( 𝑏 + 𝑧 ) = ( 𝑏 + 𝑤 ) )
126	125	cbvmptv	⊢ ( 𝑧 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑧 ) ) = ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) )
127	124 126	eqtrdi	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = ( 𝑐 ⊕ 𝑎 ) ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) )
128	127	rneqd	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = ( 𝑐 ⊕ 𝑎 ) ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ran ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) )
129		ovex	⊢ ( 𝑐 ⊕ 𝑎 ) ∈ V
130	129	mptex	⊢ ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) ∈ V
131	130	rnex	⊢ ran ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) ∈ V
132	128 9 131	ovmpoa	⊢ ( ( 𝑏 ∈ 𝑋 ∧ ( 𝑐 ⊕ 𝑎 ) ∈ 𝑆 ) → ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) = ran ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) )
133	104 120 132	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) = ran ( 𝑤 ∈ ( 𝑐 ⊕ 𝑎 ) ↦ ( 𝑏 + 𝑤 ) ) )
134	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
135	1 7	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) → ( 𝑏 + 𝑐 ) ∈ 𝑋 )
136	134 104 87 135	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑏 + 𝑐 ) ∈ 𝑋 )
137		simpr	⊢ ( ( 𝑥 = ( 𝑏 + 𝑐 ) ∧ 𝑦 = 𝑎 ) → 𝑦 = 𝑎 )
138		simpl	⊢ ( ( 𝑥 = ( 𝑏 + 𝑐 ) ∧ 𝑦 = 𝑎 ) → 𝑥 = ( 𝑏 + 𝑐 ) )
139	138	oveq1d	⊢ ( ( 𝑥 = ( 𝑏 + 𝑐 ) ∧ 𝑦 = 𝑎 ) → ( 𝑥 + 𝑧 ) = ( ( 𝑏 + 𝑐 ) + 𝑧 ) )
140	137 139	mpteq12dv	⊢ ( ( 𝑥 = ( 𝑏 + 𝑐 ) ∧ 𝑦 = 𝑎 ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) )
141	140	rneqd	⊢ ( ( 𝑥 = ( 𝑏 + 𝑐 ) ∧ 𝑦 = 𝑎 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ran ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) )
142	66	mptex	⊢ ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) ∈ V
143	142	rnex	⊢ ran ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) ∈ V
144	141 9 143	ovmpoa	⊢ ( ( ( 𝑏 + 𝑐 ) ∈ 𝑋 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ran ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) )
145	136 88 144	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ran ( 𝑧 ∈ 𝑎 ↦ ( ( 𝑏 + 𝑐 ) + 𝑧 ) ) )
146	118 133 145	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) )
147	146	ralrimivva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) )
148	83 147	jca	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( 0g ‘ 𝐺 ) ⊕ 𝑎 ) = 𝑎 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) ) )
149	148	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( ( ( 0g ‘ 𝐺 ) ⊕ 𝑎 ) = 𝑎 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) ) )
150	55 149	jca	⊢ ( 𝜑 → ( ⊕ : ( 𝑋 × 𝑆 ) ⟶ 𝑆 ∧ ∀ 𝑎 ∈ 𝑆 ( ( ( 0g ‘ 𝐺 ) ⊕ 𝑎 ) = 𝑎 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) ) ) )
151	1 7 57	isga	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ V ) ∧ ( ⊕ : ( 𝑋 × 𝑆 ) ⟶ 𝑆 ∧ ∀ 𝑎 ∈ 𝑆 ( ( ( 0g ‘ 𝐺 ) ⊕ 𝑎 ) = 𝑎 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( ( 𝑏 + 𝑐 ) ⊕ 𝑎 ) = ( 𝑏 ⊕ ( 𝑐 ⊕ 𝑎 ) ) ) ) ) )
152	13 150 151	sylanbrc	⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) )