Definition df-quot 26028

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

Step	Hyp	Ref	Expression
1		cquot 26027	. 2 class quot
2		vf	. . 3 setvar 𝑓
3		vg	. . 3 setvar 𝑔
4		cc 11110	. . . 4 class ℂ
5		cply 25922	. . . 4 class Poly
6	4, 5	cfv 6543	. . 3 class (Poly‘ℂ)
7		c0p 25410	. . . . 5 class 0𝑝
8	7	csn 4628	. . . 4 class {0𝑝}
9	6, 8	cdif 3945	. . 3 class ((Poly‘ℂ) ∖ {0𝑝})
10		vr	. . . . . . . 8 setvar 𝑟
11	10	cv 1540	. . . . . . 7 class 𝑟
12	11, 7	wceq 1541	. . . . . 6 wff 𝑟 = 0𝑝
13		cdgr 25925	. . . . . . . 8 class deg
14	11, 13	cfv 6543	. . . . . . 7 class (deg‘𝑟)
15	3	cv 1540	. . . . . . . 8 class 𝑔
16	15, 13	cfv 6543	. . . . . . 7 class (deg‘𝑔)
17		clt 11252	. . . . . . 7 class <
18	14, 16, 17	wbr 5148	. . . . . 6 wff (deg‘𝑟) < (deg‘𝑔)
19	12, 18	wo 845	. . . . 5 wff (𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
20	2	cv 1540	. . . . . 6 class 𝑓
21		vq	. . . . . . . 8 setvar 𝑞
22	21	cv 1540	. . . . . . 7 class 𝑞
23		cmul 11117	. . . . . . . 8 class ·
24	23	cof 7670	. . . . . . 7 class ∘f ·
25	15, 22, 24	co 7411	. . . . . 6 class (𝑔 ∘f · 𝑞)
26		cmin 11448	. . . . . . 7 class −
27	26	cof 7670	. . . . . 6 class ∘f −
28	20, 25, 27	co 7411	. . . . 5 class (𝑓 ∘f − (𝑔 ∘f · 𝑞))
29	19, 10, 28	wsbc 3777	. . . 4 wff [(𝑓 ∘f − (𝑔 ∘f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
30	29, 21, 6	crio 7366	. . 3 class (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)))
31	2, 3, 6, 9, 30	cmpo 7413	. 2 class (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
32	1, 31	wceq 1541	1 wff quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))

This definition is referenced by:  quotval  26029