Step | Hyp | Ref
| Expression |
1 | | plyssc 24175 |
. . 3
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
2 | 1 | sseli 3740 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
3 | 1 | sseli 3740 |
. . 3
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺 ∈
(Poly‘ℂ)) |
4 | | eldifsn 4462 |
. . . . 5
⊢ (𝐺 ∈ ((Poly‘ℂ)
∖ {0𝑝}) ↔ (𝐺 ∈ (Poly‘ℂ) ∧ 𝐺 ≠
0𝑝)) |
5 | | oveq1 6821 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑔 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · 𝑞)) |
6 | | oveq12 6823 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ (𝑔 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · 𝑞)) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) = (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞))) |
7 | 5, 6 | sylan2 492 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) = (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞))) |
8 | | quotval.1 |
. . . . . . . . . 10
⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) |
9 | 7, 8 | syl6eqr 2812 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) = 𝑅) |
10 | 9 | sbceq1d 3581 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
[𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
11 | | ovex 6842 |
. . . . . . . . . . 11
⊢ (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) ∈ V |
12 | 8, 11 | eqeltri 2835 |
. . . . . . . . . 10
⊢ 𝑅 ∈ V |
13 | | eqeq1 2764 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (𝑟 = 0𝑝 ↔ 𝑅 =
0𝑝)) |
14 | | fveq2 6353 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (deg‘𝑟) = (deg‘𝑅)) |
15 | 14 | breq1d 4814 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → ((deg‘𝑟) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝑔))) |
16 | 13, 15 | orbi12d 748 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ((𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔)))) |
17 | 12, 16 | sbcie 3611 |
. . . . . . . . 9
⊢
([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔))) |
18 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
19 | 18 | fveq2d 6357 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (deg‘𝑔) = (deg‘𝐺)) |
20 | 19 | breq2d 4816 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((deg‘𝑅) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝐺))) |
21 | 20 | orbi2d 740 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
22 | 17, 21 | syl5bb 272 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
23 | 10, 22 | bitrd 268 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
24 | 23 | riotabidv 6777 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘𝑓
− (𝑔
∘𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔))) =
(℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) |
25 | | df-quot 24265 |
. . . . . 6
⊢ quot =
(𝑓 ∈
(Poly‘ℂ), 𝑔
∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
26 | | riotaex 6779 |
. . . . . 6
⊢
(℩𝑞
∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) ∈
V |
27 | 24, 25, 26 | ovmpt2a 6957 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
((Poly‘ℂ) ∖ {0𝑝})) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
28 | 4, 27 | sylan2br 494 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝)) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
29 | 28 | 3impb 1108 |
. . 3
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
30 | 3, 29 | syl3an2 1168 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)
→ (𝐹 quot 𝐺) = (℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) |
31 | 2, 30 | syl3an1 1167 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |