Step | Hyp | Ref
| Expression |
1 | | plyssc 24393 |
. . 3
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
2 | 1 | sseli 3817 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
3 | 1 | sseli 3817 |
. . 3
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺 ∈
(Poly‘ℂ)) |
4 | | eldifsn 4550 |
. . . . 5
⊢ (𝐺 ∈ ((Poly‘ℂ)
∖ {0𝑝}) ↔ (𝐺 ∈ (Poly‘ℂ) ∧ 𝐺 ≠
0𝑝)) |
5 | | oveq1 6929 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑔 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · 𝑞)) |
6 | | oveq12 6931 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ (𝑔 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · 𝑞)) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) = (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞))) |
7 | 5, 6 | sylan2 586 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) = (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞))) |
8 | | quotval.1 |
. . . . . . . . . 10
⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) |
9 | 7, 8 | syl6eqr 2832 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) = 𝑅) |
10 | 9 | sbceq1d 3657 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
[𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
11 | | ovex 6954 |
. . . . . . . . . . 11
⊢ (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) ∈ V |
12 | 8, 11 | eqeltri 2855 |
. . . . . . . . . 10
⊢ 𝑅 ∈ V |
13 | | eqeq1 2782 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (𝑟 = 0𝑝 ↔ 𝑅 =
0𝑝)) |
14 | | fveq2 6446 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (deg‘𝑟) = (deg‘𝑅)) |
15 | 14 | breq1d 4896 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → ((deg‘𝑟) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝑔))) |
16 | 13, 15 | orbi12d 905 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ((𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔)))) |
17 | 12, 16 | sbcie 3687 |
. . . . . . . . 9
⊢
([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔))) |
18 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
19 | 18 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (deg‘𝑔) = (deg‘𝐺)) |
20 | 19 | breq2d 4898 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((deg‘𝑅) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝐺))) |
21 | 20 | orbi2d 902 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
22 | 17, 21 | syl5bb 275 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
23 | 10, 22 | bitrd 271 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
24 | 23 | riotabidv 6885 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘𝑓
− (𝑔
∘𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔))) =
(℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) |
25 | | df-quot 24483 |
. . . . . 6
⊢ quot =
(𝑓 ∈
(Poly‘ℂ), 𝑔
∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘𝑓 − (𝑔 ∘𝑓
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
26 | | riotaex 6887 |
. . . . . 6
⊢
(℩𝑞
∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) ∈
V |
27 | 24, 25, 26 | ovmpt2a 7068 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
((Poly‘ℂ) ∖ {0𝑝})) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
28 | 4, 27 | sylan2br 588 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝)) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
29 | 28 | 3impb 1104 |
. . 3
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
30 | 3, 29 | syl3an2 1164 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)
→ (𝐹 quot 𝐺) = (℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) |
31 | 2, 30 | syl3an1 1163 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |