Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-quot Structured version   Visualization version   GIF version

Definition df-quot 24890
 Description: Define the quotient function on polynomials. This is the 𝑞 of the expression 𝑓 = 𝑔 · 𝑞 + 𝑟 in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014.)
Assertion
Ref Expression
df-quot quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓f − (𝑔f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
Distinct variable group:   𝑓,𝑔,𝑞,𝑟

Detailed syntax breakdown of Definition df-quot
StepHypRef Expression
1 cquot 24889 . 2 class quot
2 vf . . 3 setvar 𝑓
3 vg . . 3 setvar 𝑔
4 cc 10528 . . . 4 class
5 cply 24784 . . . 4 class Poly
64, 5cfv 6328 . . 3 class (Poly‘ℂ)
7 c0p 24276 . . . . 5 class 0𝑝
87csn 4528 . . . 4 class {0𝑝}
96, 8cdif 3881 . . 3 class ((Poly‘ℂ) ∖ {0𝑝})
10 vr . . . . . . . 8 setvar 𝑟
1110cv 1537 . . . . . . 7 class 𝑟
1211, 7wceq 1538 . . . . . 6 wff 𝑟 = 0𝑝
13 cdgr 24787 . . . . . . . 8 class deg
1411, 13cfv 6328 . . . . . . 7 class (deg‘𝑟)
153cv 1537 . . . . . . . 8 class 𝑔
1615, 13cfv 6328 . . . . . . 7 class (deg‘𝑔)
17 clt 10668 . . . . . . 7 class <
1814, 16, 17wbr 5033 . . . . . 6 wff (deg‘𝑟) < (deg‘𝑔)
1912, 18wo 844 . . . . 5 wff (𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
202cv 1537 . . . . . 6 class 𝑓
21 vq . . . . . . . 8 setvar 𝑞
2221cv 1537 . . . . . . 7 class 𝑞
23 cmul 10535 . . . . . . . 8 class ·
2423cof 7391 . . . . . . 7 class f ·
2515, 22, 24co 7139 . . . . . 6 class (𝑔f · 𝑞)
26 cmin 10863 . . . . . . 7 class
2726cof 7391 . . . . . 6 class f
2820, 25, 27co 7139 . . . . 5 class (𝑓f − (𝑔f · 𝑞))
2919, 10, 28wsbc 3723 . . . 4 wff [(𝑓f − (𝑔f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
3029, 21, 6crio 7096 . . 3 class (𝑞 ∈ (Poly‘ℂ)[(𝑓f − (𝑔f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)))
312, 3, 6, 9, 30cmpo 7141 . 2 class (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓f − (𝑔f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
321, 31wceq 1538 1 wff quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓f − (𝑔f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
 Colors of variables: wff setvar class This definition is referenced by:  quotval  24891
 Copyright terms: Public domain W3C validator