| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | plyssc 26240 | . . 3
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) | 
| 2 | 1 | sseli 3978 | . 2
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) | 
| 3 | 1 | sseli 3978 | . . 3
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺 ∈
(Poly‘ℂ)) | 
| 4 |  | eldifsn 4785 | . . . . 5
⊢ (𝐺 ∈ ((Poly‘ℂ)
∖ {0𝑝}) ↔ (𝐺 ∈ (Poly‘ℂ) ∧ 𝐺 ≠
0𝑝)) | 
| 5 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑔 ∘f · 𝑞) = (𝐺 ∘f · 𝑞)) | 
| 6 |  | oveq12 7441 | . . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ (𝑔 ∘f · 𝑞) = (𝐺 ∘f · 𝑞)) → (𝑓 ∘f − (𝑔 ∘f ·
𝑞)) = (𝐹 ∘f − (𝐺 ∘f ·
𝑞))) | 
| 7 | 5, 6 | sylan2 593 | . . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘f − (𝑔 ∘f ·
𝑞)) = (𝐹 ∘f − (𝐺 ∘f ·
𝑞))) | 
| 8 |  | quotval.1 | . . . . . . . . . 10
⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f ·
𝑞)) | 
| 9 | 7, 8 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘f − (𝑔 ∘f ·
𝑞)) = 𝑅) | 
| 10 | 9 | sbceq1d 3792 | . . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
[𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) | 
| 11 | 8 | ovexi 7466 | . . . . . . . . . 10
⊢ 𝑅 ∈ V | 
| 12 |  | eqeq1 2740 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (𝑟 = 0𝑝 ↔ 𝑅 =
0𝑝)) | 
| 13 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (deg‘𝑟) = (deg‘𝑅)) | 
| 14 | 13 | breq1d 5152 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → ((deg‘𝑟) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝑔))) | 
| 15 | 12, 14 | orbi12d 918 | . . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ((𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔)))) | 
| 16 | 11, 15 | sbcie 3829 | . . . . . . . . 9
⊢
([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝑔))) | 
| 17 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) | 
| 18 | 17 | fveq2d 6909 | . . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (deg‘𝑔) = (deg‘𝐺)) | 
| 19 | 18 | breq2d 5154 | . . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((deg‘𝑅) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝐺))) | 
| 20 | 19 | orbi2d 915 | . . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) | 
| 21 | 16, 20 | bitrid 283 | . . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([𝑅 / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) | 
| 22 | 10, 21 | bitrd 279 | . . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) | 
| 23 | 22 | riotabidv 7391 | . . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘f −
(𝑔 ∘f
· 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔))) =
(℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) | 
| 24 |  | df-quot 26334 | . . . . . 6
⊢  quot =
(𝑓 ∈
(Poly‘ℂ), 𝑔
∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) | 
| 25 |  | riotaex 7393 | . . . . . 6
⊢
(℩𝑞
∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) ∈
V | 
| 26 | 23, 24, 25 | ovmpoa 7589 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
((Poly‘ℂ) ∖ {0𝑝})) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) | 
| 27 | 4, 26 | sylan2br 595 | . . . 4
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝)) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) | 
| 28 | 27 | 3impb 1114 | . . 3
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) | 
| 29 | 3, 28 | syl3an2 1164 | . 2
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)
→ (𝐹 quot 𝐺) = (℩𝑞 ∈
(Poly‘ℂ)(𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))) | 
| 30 | 2, 29 | syl3an1 1163 | 1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |