Metamath Proof Explorer

Theorem sylow3lem1

Description: Lemma for sylow3 , first part. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
sylow3.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
sylow3.xf ⊢ ( 𝜑 → 𝑋 ∈ Fin )
sylow3.p ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
sylow3lem1.a ⊢ + = ( +g ‘ 𝐺 )
sylow3lem1.d ⊢ − = ( -g ‘ 𝐺 )
sylow3lem1.m ⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
Assertion sylow3lem1 ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) )

Proof

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