Detailed syntax breakdown of Definition df-quot
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cquot 25450 |
. 2
class
quot |
| 2 | | vf |
. . 3
setvar 𝑓 |
| 3 | | vg |
. . 3
setvar 𝑔 |
| 4 | | cc 10869 |
. . . 4
class
ℂ |
| 5 | | cply 25345 |
. . . 4
class
Poly |
| 6 | 4, 5 | cfv 6433 |
. . 3
class
(Poly‘ℂ) |
| 7 | | c0p 24833 |
. . . . 5
class
0𝑝 |
| 8 | 7 | csn 4561 |
. . . 4
class
{0𝑝} |
| 9 | 6, 8 | cdif 3884 |
. . 3
class
((Poly‘ℂ) ∖ {0𝑝}) |
| 10 | | vr |
. . . . . . . 8
setvar 𝑟 |
| 11 | 10 | cv 1538 |
. . . . . . 7
class 𝑟 |
| 12 | 11, 7 | wceq 1539 |
. . . . . 6
wff 𝑟 =
0𝑝 |
| 13 | | cdgr 25348 |
. . . . . . . 8
class
deg |
| 14 | 11, 13 | cfv 6433 |
. . . . . . 7
class
(deg‘𝑟) |
| 15 | 3 | cv 1538 |
. . . . . . . 8
class 𝑔 |
| 16 | 15, 13 | cfv 6433 |
. . . . . . 7
class
(deg‘𝑔) |
| 17 | | clt 11009 |
. . . . . . 7
class
< |
| 18 | 14, 16, 17 | wbr 5074 |
. . . . . 6
wff
(deg‘𝑟) <
(deg‘𝑔) |
| 19 | 12, 18 | wo 844 |
. . . . 5
wff (𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) |
| 20 | 2 | cv 1538 |
. . . . . 6
class 𝑓 |
| 21 | | vq |
. . . . . . . 8
setvar 𝑞 |
| 22 | 21 | cv 1538 |
. . . . . . 7
class 𝑞 |
| 23 | | cmul 10876 |
. . . . . . . 8
class
· |
| 24 | 23 | cof 7531 |
. . . . . . 7
class
∘f · |
| 25 | 15, 22, 24 | co 7275 |
. . . . . 6
class (𝑔 ∘f ·
𝑞) |
| 26 | | cmin 11205 |
. . . . . . 7
class
− |
| 27 | 26 | cof 7531 |
. . . . . 6
class
∘f − |
| 28 | 20, 25, 27 | co 7275 |
. . . . 5
class (𝑓 ∘f −
(𝑔 ∘f
· 𝑞)) |
| 29 | 19, 10, 28 | wsbc 3716 |
. . . 4
wff
[(𝑓
∘f − (𝑔 ∘f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) |
| 30 | 29, 21, 6 | crio 7231 |
. . 3
class
(℩𝑞
∈ (Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔))) |
| 31 | 2, 3, 6, 9, 30 | cmpo 7277 |
. 2
class (𝑓 ∈ (Poly‘ℂ),
𝑔 ∈
((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
| 32 | 1, 31 | wceq 1539 |
1
wff quot =
(𝑓 ∈
(Poly‘ℂ), 𝑔
∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
