Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | plydiv.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |
3 | | plydiv.z |
. . . . 5
⊢ (𝜑 → 𝐺 ≠
0𝑝) |
4 | | eqid 2610 |
. . . . . 6
⊢ (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) |
5 | 4 | quotval 23851 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
6 | 1, 2, 3, 5 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
7 | | plydiv.pl |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
8 | | plydiv.tm |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
9 | | plydiv.rc |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) |
10 | | plydiv.m1 |
. . . . . . 7
⊢ (𝜑 → -1 ∈ 𝑆) |
11 | 7, 8, 9, 10, 1, 2,
3, 4 | plydivalg 23858 |
. . . . . 6
⊢ (𝜑 → ∃!𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) |
12 | | reurex 3137 |
. . . . . 6
⊢
(∃!𝑞 ∈
(Poly‘𝑆)((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)) → ∃𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) |
14 | | addcl 9897 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
15 | 14 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) |
16 | | mulcl 9899 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
17 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
18 | | reccl 10571 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈
ℂ) |
19 | 18 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ ℂ) |
20 | | neg1cn 11001 |
. . . . . . 7
⊢ -1 ∈
ℂ |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (𝜑 → -1 ∈
ℂ) |
22 | | plyssc 23760 |
. . . . . . 7
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
23 | 22, 1 | sseldi 3566 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℂ)) |
24 | 22, 2 | sseldi 3566 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈
(Poly‘ℂ)) |
25 | 15, 17, 19, 21, 23, 24, 3, 4 | plydivalg 23858 |
. . . . 5
⊢ (𝜑 → ∃!𝑞 ∈ (Poly‘ℂ)((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺))) |
26 | | id 22 |
. . . . . . 7
⊢ (((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)) → ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) |
27 | 26 | rgenw 2908 |
. . . . . 6
⊢
∀𝑞 ∈
(Poly‘𝑆)(((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)) → ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) |
28 | | riotass2 6537 |
. . . . . 6
⊢
((((Poly‘𝑆)
⊆ (Poly‘ℂ) ∧ ∀𝑞 ∈ (Poly‘𝑆)(((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) →
((𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) ∧ (∃𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) ∧
∃!𝑞 ∈
(Poly‘ℂ)((𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) → (℩𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) =
(℩𝑞 ∈
(Poly‘ℂ)((𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
29 | 22, 27, 28 | mpanl12 714 |
. . . . 5
⊢
((∃𝑞 ∈
(Poly‘𝑆)((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)) ∧ ∃!𝑞 ∈
(Poly‘ℂ)((𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺))) → (℩𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) =
(℩𝑞 ∈
(Poly‘ℂ)((𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
30 | 13, 25, 29 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (℩𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) =
(℩𝑞 ∈
(Poly‘ℂ)((𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
31 | 6, 30 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) |
32 | | riotacl2 6524 |
. . . 4
⊢
(∃!𝑞 ∈
(Poly‘𝑆)((𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)) → (℩𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∈
{𝑞 ∈ (Poly‘𝑆) ∣ ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))}) |
33 | 11, 32 | syl 17 |
. . 3
⊢ (𝜑 → (℩𝑞 ∈ (Poly‘𝑆)((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∈
{𝑞 ∈ (Poly‘𝑆) ∣ ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))}) |
34 | 31, 33 | eqeltrd 2688 |
. 2
⊢ (𝜑 → (𝐹 quot 𝐺) ∈ {𝑞 ∈ (Poly‘𝑆) ∣ ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))}) |
35 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑞 = (𝐹 quot 𝐺) → (𝐺 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · (𝐹 quot 𝐺))) |
36 | 35 | oveq2d 6565 |
. . . . . 6
⊢ (𝑞 = (𝐹 quot 𝐺) → (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) = (𝐹 ∘𝑓
− (𝐺
∘𝑓 · (𝐹 quot 𝐺)))) |
37 | | quotlem.8 |
. . . . . 6
⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐹 quot 𝐺))) |
38 | 36, 37 | syl6eqr 2662 |
. . . . 5
⊢ (𝑞 = (𝐹 quot 𝐺) → (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) = 𝑅) |
39 | 38 | eqeq1d 2612 |
. . . 4
⊢ (𝑞 = (𝐹 quot 𝐺) → ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ↔ 𝑅 = 0𝑝)) |
40 | 38 | fveq2d 6107 |
. . . . 5
⊢ (𝑞 = (𝐹 quot 𝐺) → (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) =
(deg‘𝑅)) |
41 | 40 | breq1d 4593 |
. . . 4
⊢ (𝑞 = (𝐹 quot 𝐺) → ((deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺) ↔
(deg‘𝑅) <
(deg‘𝐺))) |
42 | 39, 41 | orbi12d 742 |
. . 3
⊢ (𝑞 = (𝐹 quot 𝐺) → (((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
43 | 42 | elrab 3331 |
. 2
⊢ ((𝐹 quot 𝐺) ∈ {𝑞 ∈ (Poly‘𝑆) ∣ ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))} ↔
((𝐹 quot 𝐺) ∈ (Poly‘𝑆) ∧ (𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
44 | 34, 43 | sylib 207 |
1
⊢ (𝜑 → ((𝐹 quot 𝐺) ∈ (Poly‘𝑆) ∧ (𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |