Metamath Proof Explorer

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 fovrnd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 ⊕ 𝑎 ) ∈ 𝑆 )
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 𝑆 ) )