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

Definition df-quot 24091
 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‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
Distinct variable group:   𝑓,𝑔,𝑞,𝑟

Detailed syntax breakdown of Definition df-quot
StepHypRef Expression
1 cquot 24090 . 2 class quot
2 vf . . 3 setvar 𝑓
3 vg . . 3 setvar 𝑔
4 cc 9972 . . . 4 class
5 cply 23985 . . . 4 class Poly
64, 5cfv 5926 . . 3 class (Poly‘ℂ)
7 c0p 23481 . . . . 5 class 0𝑝
87csn 4210 . . . 4 class {0𝑝}
96, 8cdif 3604 . . 3 class ((Poly‘ℂ) ∖ {0𝑝})
10 vr . . . . . . . 8 setvar 𝑟
1110cv 1522 . . . . . . 7 class 𝑟
1211, 7wceq 1523 . . . . . 6 wff 𝑟 = 0𝑝
13 cdgr 23988 . . . . . . . 8 class deg
1411, 13cfv 5926 . . . . . . 7 class (deg‘𝑟)
153cv 1522 . . . . . . . 8 class 𝑔
1615, 13cfv 5926 . . . . . . 7 class (deg‘𝑔)
17 clt 10112 . . . . . . 7 class <
1814, 16, 17wbr 4685 . . . . . 6 wff (deg‘𝑟) < (deg‘𝑔)
1912, 18wo 382 . . . . 5 wff (𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
202cv 1522 . . . . . 6 class 𝑓
21 vq . . . . . . . 8 setvar 𝑞
2221cv 1522 . . . . . . 7 class 𝑞
23 cmul 9979 . . . . . . . 8 class ·
2423cof 6937 . . . . . . 7 class 𝑓 ·
2515, 22, 24co 6690 . . . . . 6 class (𝑔𝑓 · 𝑞)
26 cmin 10304 . . . . . . 7 class
2726cof 6937 . . . . . 6 class 𝑓
2820, 25, 27co 6690 . . . . 5 class (𝑓𝑓 − (𝑔𝑓 · 𝑞))
2919, 10, 28wsbc 3468 . . . 4 wff [(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
3029, 21, 6crio 6650 . . 3 class (𝑞 ∈ (Poly‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)))
312, 3, 6, 9, 30cmpt2 6692 . 2 class (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
321, 31wceq 1523 1 wff quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
 Colors of variables: wff setvar class This definition is referenced by:  quotval  24092
 Copyright terms: Public domain W3C validator