Step | Hyp | Ref
| Expression |
1 | | plyssc 25125 |
. . 3
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
2 | 1 | sseli 3913 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
3 | 1 | sseli 3913 |
. . 3
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺 ∈
(Poly‘ℂ)) |
4 | | eldifsn 4716 |
. . . . 5
⊢ (𝐺 ∈ ((Poly‘ℂ)
∖ {0𝑝}) ↔ (𝐺 ∈ (Poly‘ℂ) ∧ 𝐺 ≠
0𝑝)) |
5 | | oveq1 7241 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑔 ∘f · 𝑞) = (𝐺 ∘f · 𝑞)) |
6 | | oveq12 7243 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ (𝑔 ∘f · 𝑞) = (𝐺 ∘f · 𝑞)) → (𝑓 ∘f − (𝑔 ∘f ·
𝑞)) = (𝐹 ∘f − (𝐺 ∘f ·
𝑞))) |
7 | 5, 6 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘f − (𝑔 ∘f ·
𝑞)) = (𝐹 ∘f − (𝐺 ∘f ·
𝑞))) |
8 | | quotval.1 |
. . . . . . . . . 10
⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f ·
𝑞)) |
9 | 7, 8 | eqtr4di 2798 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘f − (𝑔 ∘f ·
𝑞)) = 𝑅) |
10 | 9 | sbceq1d 3716 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
[𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
11 | 8 | ovexi 7268 |
. . . . . . . . . 10
⊢ 𝑅 ∈ V |
12 | | eqeq1 2743 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (𝑟 = 0𝑝 ↔ 𝑅 =
0𝑝)) |
13 | | fveq2 6738 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (deg‘𝑟) = (deg‘𝑅)) |
14 | 13 | breq1d 5079 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → ((deg‘𝑟) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝑔))) |
15 | 12, 14 | orbi12d 919 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ((𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔)))) |
16 | 11, 15 | sbcie 3754 |
. . . . . . . . 9
⊢
([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔))) |
17 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
18 | 17 | fveq2d 6742 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (deg‘𝑔) = (deg‘𝐺)) |
19 | 18 | breq2d 5081 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((deg‘𝑅) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝐺))) |
20 | 19 | orbi2d 916 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
21 | 16, 20 | syl5bb 286 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
22 | 10, 21 | bitrd 282 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
23 | 22 | riotabidv 7193 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘f −
(𝑔 ∘f
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔))) =
(℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) |
24 | | df-quot 25215 |
. . . . . 6
⊢ quot =
(𝑓 ∈
(Poly‘ℂ), 𝑔
∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
25 | | riotaex 7195 |
. . . . . 6
⊢
(℩𝑞
∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) ∈
V |
26 | 23, 24, 25 | ovmpoa 7385 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
((Poly‘ℂ) ∖ {0𝑝})) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
27 | 4, 26 | sylan2br 598 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝)) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
28 | 27 | 3impb 1117 |
. . 3
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
29 | 3, 28 | syl3an2 1166 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)
→ (𝐹 quot 𝐺) = (℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) |
30 | 2, 29 | syl3an1 1165 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |