Step | Hyp | Ref
| Expression |
1 | | sylow3.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
2 | | ovex 6678 |
. . 3
⊢ (𝑃 pSyl 𝐺) ∈ V |
3 | 1, 2 | jctir 561 |
. 2
⊢ (𝜑 → (𝐺 ∈ Grp ∧ (𝑃 pSyl 𝐺) ∈ V)) |
4 | | sylow3.xf |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ Fin) |
5 | | sylow3.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℙ) |
6 | | sylow3.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝐺) |
7 | 6 | fislw 18040 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝑦 ∈ (𝑃 pSyl 𝐺) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))) |
8 | 1, 4, 5, 7 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑃 pSyl 𝐺) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))) |
9 | 8 | biimpa 501 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺)) → (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
10 | 9 | adantrl 752 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
11 | 10 | simpld 475 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ∈ (SubGrp‘𝐺)) |
12 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑥 ∈ 𝑋) |
13 | | sylow3lem1.a |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
14 | | sylow3lem1.d |
. . . . . . . 8
⊢ − =
(-g‘𝐺) |
15 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) |
16 | 6, 13, 14, 15 | conjsubg 17692 |
. . . . . . 7
⊢ ((𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (SubGrp‘𝐺)) |
17 | 11, 12, 16 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (SubGrp‘𝐺)) |
18 | 6, 13, 14, 15 | conjsubgen 17693 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) |
19 | 11, 12, 18 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) |
20 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑋 ∈ Fin) |
21 | 6 | subgss 17595 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (SubGrp‘𝐺) → 𝑦 ⊆ 𝑋) |
22 | 11, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ⊆ 𝑋) |
23 | | ssfi 8180 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ 𝑦 ⊆ 𝑋) → 𝑦 ∈ Fin) |
24 | 20, 22, 23 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ∈ Fin) |
25 | 6 | subgss 17595 |
. . . . . . . . . . 11
⊢ (ran
(𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (SubGrp‘𝐺) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ⊆ 𝑋) |
26 | 17, 25 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ⊆ 𝑋) |
27 | | ssfi 8180 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ⊆ 𝑋) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ Fin) |
28 | 20, 26, 27 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ Fin) |
29 | | hashen 13135 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ Fin) → ((#‘𝑦) = (#‘ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) ↔ 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))) |
30 | 24, 28, 29 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → ((#‘𝑦) = (#‘ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) ↔ 𝑦 ≈ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))) |
31 | 19, 30 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → (#‘𝑦) = (#‘ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))) |
32 | 10 | simprd 479 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
33 | 31, 32 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → (#‘ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
34 | 6 | fislw 18040 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (ran
(𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (SubGrp‘𝐺) ∧ (#‘ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))) |
35 | 1, 4, 5, 34 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (SubGrp‘𝐺) ∧ (#‘ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))) |
36 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → (ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (SubGrp‘𝐺) ∧ (#‘ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))) |
37 | 17, 33, 36 | mpbir2and 957 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (𝑃 pSyl 𝐺)) |
38 | 37 | ralrimivva 2971 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (𝑃 pSyl 𝐺)ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (𝑃 pSyl 𝐺)) |
39 | | sylow3lem1.m |
. . . . 5
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) |
40 | 39 | fmpt2 7237 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ (𝑃 pSyl 𝐺)ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ ⊕ :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺)) |
41 | 38, 40 | sylib 208 |
. . 3
⊢ (𝜑 → ⊕ :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺)) |
42 | 1 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝐺 ∈ Grp) |
43 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
44 | 6, 43 | grpidcl 17450 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
45 | 42, 44 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → (0g‘𝐺) ∈ 𝑋) |
46 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎 ∈ (𝑃 pSyl 𝐺)) |
47 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
48 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g‘𝐺)) |
49 | 48 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g‘𝐺) + 𝑧)) |
50 | 49, 48 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → ((𝑥 + 𝑧) − 𝑥) = (((0g‘𝐺) + 𝑧) −
(0g‘𝐺))) |
51 | 47, 50 | mpteq12dv 4733 |
. . . . . . . . 9
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺)))) |
52 | 51 | rneqd 5353 |
. . . . . . . 8
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺)))) |
53 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
54 | 53 | mptex 6486 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺)))
∈ V |
55 | 54 | rnex 7100 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑎 ↦
(((0g‘𝐺)
+ 𝑧) −
(0g‘𝐺)))
∈ V |
56 | 52, 39, 55 | ovmpt2a 6791 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑋 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g‘𝐺) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺)))) |
57 | 45, 46, 56 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g‘𝐺) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺)))) |
58 | 1 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧 ∈ 𝑎) → 𝐺 ∈ Grp) |
59 | | slwsubg 18025 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (𝑃 pSyl 𝐺) → 𝑎 ∈ (SubGrp‘𝐺)) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎 ∈ (SubGrp‘𝐺)) |
61 | 6 | subgss 17595 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (SubGrp‘𝐺) → 𝑎 ⊆ 𝑋) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎 ⊆ 𝑋) |
63 | 62 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝑋) |
64 | 6, 13, 43 | grplid 17452 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺) + 𝑧) = 𝑧) |
65 | 58, 63, 64 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧 ∈ 𝑎) → ((0g‘𝐺) + 𝑧) = 𝑧) |
66 | 65 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧 ∈ 𝑎) → (((0g‘𝐺) + 𝑧) −
(0g‘𝐺)) =
(𝑧 −
(0g‘𝐺))) |
67 | 6, 43, 14 | grpsubid1 17500 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (𝑧 −
(0g‘𝐺)) =
𝑧) |
68 | 58, 63, 67 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧 ∈ 𝑎) → (𝑧 −
(0g‘𝐺)) =
𝑧) |
69 | 66, 68 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧 ∈ 𝑎) → (((0g‘𝐺) + 𝑧) −
(0g‘𝐺)) =
𝑧) |
70 | 69 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺))) =
(𝑧 ∈ 𝑎 ↦ 𝑧)) |
71 | | mptresid 5456 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ 𝑧) = ( I ↾ 𝑎) |
72 | 70, 71 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺))) =
( I ↾ 𝑎)) |
73 | 72 | rneqd 5353 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → ran (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺))) =
ran ( I ↾ 𝑎)) |
74 | | rnresi 5479 |
. . . . . . 7
⊢ ran ( I
↾ 𝑎) = 𝑎 |
75 | 73, 74 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → ran (𝑧 ∈ 𝑎 ↦ (((0g‘𝐺) + 𝑧) −
(0g‘𝐺))) =
𝑎) |
76 | 57, 75 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g‘𝐺) ⊕ 𝑎) = 𝑎) |
77 | | ovex 6678 |
. . . . . . . . . 10
⊢ ((𝑐 + 𝑧) − 𝑐) ∈ V |
78 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑤 = ((𝑐 + 𝑧) − 𝑐) → (𝑏 + 𝑤) = (𝑏 + ((𝑐 + 𝑧) − 𝑐))) |
79 | 78 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑤 = ((𝑐 + 𝑧) − 𝑐) → ((𝑏 + 𝑤) − 𝑏) = ((𝑏 + ((𝑐 + 𝑧) − 𝑐)) − 𝑏)) |
80 | 77, 79 | abrexco 6502 |
. . . . . . . . 9
⊢ {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = ((𝑐 + 𝑧) − 𝑐)}𝑢 = ((𝑏 + 𝑤) − 𝑏)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) − 𝑐)) − 𝑏)} |
81 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋) |
82 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ (𝑃 pSyl 𝐺)) |
83 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
84 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → 𝑥 = 𝑐) |
85 | 84 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧)) |
86 | 85, 84 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → ((𝑥 + 𝑧) − 𝑥) = ((𝑐 + 𝑧) − 𝑐)) |
87 | 83, 86 | mpteq12dv 4733 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐))) |
88 | 87 | rneqd 5353 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐))) |
89 | 53 | mptex 6486 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐)) ∈ V |
90 | 89 | rnex 7100 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐)) ∈ V |
91 | 88, 39, 90 | ovmpt2a 6791 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑐 ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐))) |
92 | 81, 82, 91 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐))) |
93 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐)) = (𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐)) |
94 | 93 | rnmpt 5371 |
. . . . . . . . . . . 12
⊢ ran
(𝑧 ∈ 𝑎 ↦ ((𝑐 + 𝑧) − 𝑐)) = {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = ((𝑐 + 𝑧) − 𝑐)} |
95 | 92, 94 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) = {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = ((𝑐 + 𝑧) − 𝑐)}) |
96 | 95 | rexeqdv 3145 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = ((𝑏 + 𝑤) − 𝑏) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = ((𝑐 + 𝑧) − 𝑐)}𝑢 = ((𝑏 + 𝑤) − 𝑏))) |
97 | 96 | abbidv 2741 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = ((𝑏 + 𝑤) − 𝑏)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧 ∈ 𝑎 𝑣 = ((𝑐 + 𝑧) − 𝑐)}𝑢 = ((𝑏 + 𝑤) − 𝑏)}) |
98 | 42 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐺 ∈ Grp) |
99 | 98 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝐺 ∈ Grp) |
100 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
101 | 6, 13 | grpcl 17430 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) → (𝑏 + 𝑐) ∈ 𝑋) |
102 | 98, 100, 81, 101 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑏 + 𝑐) ∈ 𝑋) |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (𝑏 + 𝑐) ∈ 𝑋) |
104 | 63 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝑋) |
105 | 6, 13 | grpcl 17430 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ (𝑏 + 𝑐) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑏 + 𝑐) + 𝑧) ∈ 𝑋) |
106 | 99, 103, 104, 105 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → ((𝑏 + 𝑐) + 𝑧) ∈ 𝑋) |
107 | 81 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑐 ∈ 𝑋) |
108 | 100 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → 𝑏 ∈ 𝑋) |
109 | 6, 13, 14 | grpsubsub4 17508 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (((𝑏 + 𝑐) + 𝑧) ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((((𝑏 + 𝑐) + 𝑧) − 𝑐) − 𝑏) = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) |
110 | 99, 106, 107, 108, 109 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → ((((𝑏 + 𝑐) + 𝑧) − 𝑐) − 𝑏) = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) |
111 | 6, 13 | grpass 17431 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧))) |
112 | 99, 108, 107, 104, 111 | syl13anc 1328 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧))) |
113 | 112 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (((𝑏 + 𝑐) + 𝑧) − 𝑐) = ((𝑏 + (𝑐 + 𝑧)) − 𝑐)) |
114 | 6, 13 | grpcl 17430 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝑐 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑐 + 𝑧) ∈ 𝑋) |
115 | 99, 107, 104, 114 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (𝑐 + 𝑧) ∈ 𝑋) |
116 | 6, 13, 14 | grpaddsubass 17505 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ (𝑐 + 𝑧) ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑏 + (𝑐 + 𝑧)) − 𝑐) = (𝑏 + ((𝑐 + 𝑧) − 𝑐))) |
117 | 99, 108, 115, 107, 116 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → ((𝑏 + (𝑐 + 𝑧)) − 𝑐) = (𝑏 + ((𝑐 + 𝑧) − 𝑐))) |
118 | 113, 117 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (((𝑏 + 𝑐) + 𝑧) − 𝑐) = (𝑏 + ((𝑐 + 𝑧) − 𝑐))) |
119 | 118 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → ((((𝑏 + 𝑐) + 𝑧) − 𝑐) − 𝑏) = ((𝑏 + ((𝑐 + 𝑧) − 𝑐)) − 𝑏)) |
120 | 110, 119 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)) = ((𝑏 + ((𝑐 + 𝑧) − 𝑐)) − 𝑏)) |
121 | 120 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑎) → (𝑢 = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)) ↔ 𝑢 = ((𝑏 + ((𝑐 + 𝑧) − 𝑐)) − 𝑏))) |
122 | 121 | rexbidva 3049 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (∃𝑧 ∈ 𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)) ↔ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) − 𝑐)) − 𝑏))) |
123 | 122 | abbidv 2741 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) − 𝑐)) − 𝑏)}) |
124 | 80, 97, 123 | 3eqtr4a 2682 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = ((𝑏 + 𝑤) − 𝑏)} = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))}) |
125 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏)) |
126 | 125 | rnmpt 5371 |
. . . . . . . 8
⊢ ran
(𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 ⊕ 𝑎)𝑢 = ((𝑏 + 𝑤) − 𝑏)} |
127 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) = (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) |
128 | 127 | rnmpt 5371 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) = {𝑢 ∣ ∃𝑧 ∈ 𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))} |
129 | 124, 126,
128 | 3eqtr4g 2681 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏)) = ran (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)))) |
130 | 41 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⊕ :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺)) |
131 | 130, 81, 82 | fovrnd 6806 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐 ⊕ 𝑎) ∈ (𝑃 pSyl 𝐺)) |
132 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → 𝑦 = (𝑐 ⊕ 𝑎)) |
133 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → 𝑥 = 𝑏) |
134 | 133 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧)) |
135 | 134, 133 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → ((𝑥 + 𝑧) − 𝑥) = ((𝑏 + 𝑧) − 𝑏)) |
136 | 132, 135 | mpteq12dv 4733 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑧) − 𝑏))) |
137 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤)) |
138 | 137 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → ((𝑏 + 𝑧) − 𝑏) = ((𝑏 + 𝑤) − 𝑏)) |
139 | 138 | cbvmptv 4750 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑧) − 𝑏)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏)) |
140 | 136, 139 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏))) |
141 | 140 | rneqd 5353 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = (𝑐 ⊕ 𝑎)) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏))) |
142 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑐 ⊕ 𝑎) ∈ V |
143 | 142 | mptex 6486 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏)) ∈ V |
144 | 143 | rnex 7100 |
. . . . . . . . 9
⊢ ran
(𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏)) ∈ V |
145 | 141, 39, 144 | ovmpt2a 6791 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝑋 ∧ (𝑐 ⊕ 𝑎) ∈ (𝑃 pSyl 𝐺)) → (𝑏 ⊕ (𝑐 ⊕ 𝑎)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏))) |
146 | 100, 131,
145 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑏 ⊕ (𝑐 ⊕ 𝑎)) = ran (𝑤 ∈ (𝑐 ⊕ 𝑎) ↦ ((𝑏 + 𝑤) − 𝑏))) |
147 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎) |
148 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐)) |
149 | 148 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧)) |
150 | 149, 148 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ((𝑥 + 𝑧) − 𝑥) = (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) |
151 | 147, 150 | mpteq12dv 4733 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)))) |
152 | 151 | rneqd 5353 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)))) |
153 | 53 | mptex 6486 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) ∈ V |
154 | 153 | rnex 7100 |
. . . . . . . . 9
⊢ ran
(𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐))) ∈ V |
155 | 152, 39, 154 | ovmpt2a 6791 |
. . . . . . . 8
⊢ (((𝑏 + 𝑐) ∈ 𝑋 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → ((𝑏 + 𝑐) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)))) |
156 | 102, 82, 155 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑏 + 𝑐) ⊕ 𝑎) = ran (𝑧 ∈ 𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) − (𝑏 + 𝑐)))) |
157 | 129, 146,
156 | 3eqtr4rd 2667 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))) |
158 | 157 | ralrimivva 2971 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))) |
159 | 76, 158 | jca 554 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑃 pSyl 𝐺)) → (((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))) |
160 | 159 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))) |
161 | 41, 160 | jca 554 |
. 2
⊢ (𝜑 → ( ⊕ :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺) ∧ ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎))))) |
162 | 6, 13, 43 | isga 17724 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct (𝑃 pSyl 𝐺)) ↔ ((𝐺 ∈ Grp ∧ (𝑃 pSyl 𝐺) ∈ V) ∧ ( ⊕ :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺) ∧ ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g‘𝐺) ⊕ 𝑎) = 𝑎 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 ((𝑏 + 𝑐) ⊕ 𝑎) = (𝑏 ⊕ (𝑐 ⊕ 𝑎)))))) |
163 | 3, 161, 162 | sylanbrc 698 |
1
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺))) |