Detailed syntax breakdown of Definition df-quot
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cquot 24881 |
. 2
class
quot |
| 2 | | vf |
. . 3
setvar 𝑓 |
| 3 | | vg |
. . 3
setvar 𝑔 |
| 4 | | cc 10537 |
. . . 4
class
ℂ |
| 5 | | cply 24776 |
. . . 4
class
Poly |
| 6 | 4, 5 | cfv 6357 |
. . 3
class
(Poly‘ℂ) |
| 7 | | c0p 24272 |
. . . . 5
class
0𝑝 |
| 8 | 7 | csn 4569 |
. . . 4
class
{0𝑝} |
| 9 | 6, 8 | cdif 3935 |
. . 3
class
((Poly‘ℂ) ∖ {0𝑝}) |
| 10 | | vr |
. . . . . . . 8
setvar 𝑟 |
| 11 | 10 | cv 1536 |
. . . . . . 7
class 𝑟 |
| 12 | 11, 7 | wceq 1537 |
. . . . . 6
wff 𝑟 =
0𝑝 |
| 13 | | cdgr 24779 |
. . . . . . . 8
class
deg |
| 14 | 11, 13 | cfv 6357 |
. . . . . . 7
class
(deg‘𝑟) |
| 15 | 3 | cv 1536 |
. . . . . . . 8
class 𝑔 |
| 16 | 15, 13 | cfv 6357 |
. . . . . . 7
class
(deg‘𝑔) |
| 17 | | clt 10677 |
. . . . . . 7
class
< |
| 18 | 14, 16, 17 | wbr 5068 |
. . . . . 6
wff
(deg‘𝑟) <
(deg‘𝑔) |
| 19 | 12, 18 | wo 843 |
. . . . 5
wff (𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) |
| 20 | 2 | cv 1536 |
. . . . . 6
class 𝑓 |
| 21 | | vq |
. . . . . . . 8
setvar 𝑞 |
| 22 | 21 | cv 1536 |
. . . . . . 7
class 𝑞 |
| 23 | | cmul 10544 |
. . . . . . . 8
class
· |
| 24 | 23 | cof 7409 |
. . . . . . 7
class
∘f · |
| 25 | 15, 22, 24 | co 7158 |
. . . . . 6
class (𝑔 ∘f ·
𝑞) |
| 26 | | cmin 10872 |
. . . . . . 7
class
− |
| 27 | 26 | cof 7409 |
. . . . . 6
class
∘f − |
| 28 | 20, 25, 27 | co 7158 |
. . . . 5
class (𝑓 ∘f −
(𝑔 ∘f
· 𝑞)) |
| 29 | 19, 10, 28 | wsbc 3774 |
. . . 4
wff
[(𝑓
∘f − (𝑔 ∘f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)) |
| 30 | 29, 21, 6 | crio 7115 |
. . 3
class
(℩𝑞
∈ (Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔))) |
| 31 | 2, 3, 6, 9, 30 | cmpo 7160 |
. 2
class (𝑓 ∈ (Poly‘ℂ),
𝑔 ∈
((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
| 32 | 1, 31 | wceq 1537 |
1
wff quot =
(𝑓 ∈
(Poly‘ℂ), 𝑔
∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦
(℩𝑞 ∈
(Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f ·
𝑞)) / 𝑟](𝑟 = 0𝑝 ∨
(deg‘𝑟) <
(deg‘𝑔)))) |
