Definition df-quot

Description: Define the quotient function on polynomials. This is the q of the expression f = g x. q + r in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014)

	Ref	Expression
Assertion	df-quot	$$⊢\mathrm{quot}=\left(f\in \mathrm{Poly}\left(ℂ\right),g\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{0_{𝑝}\right\}\right)⟼\left(\iota q\in \mathrm{Poly}\left(ℂ\right)|\underset{\dot{}}{[}\left(f{-}_f\left(g{\times }_{f}q\right)\right)/r\underset{\dot{}}{]}\left(r=0_{𝑝}\vee \mathrm{deg}\left(r\right)<\mathrm{deg}\left(g\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cquot	$$class\mathrm{quot}$$
1		vf	$$setvarf$$
2		cply	$$class\mathrm{Poly}$$
3		cc	$$classℂ$$
4	3 2	cfv	$$class\mathrm{Poly}\left(ℂ\right)$$
5		vg	$$setvarg$$
6		c0p	$$class{0}_{𝑝}$$
7	6	csn	$$class\left\{0_{𝑝}\right\}$$
8	4 7	cdif	$$class\left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{0_{𝑝}\right\}\right)$$
9		vq	$$setvarq$$
10	1	cv	$$setvarf$$
11		cmin	$$class-$$
12	11	cof	$$class{\circ }_f-$$
13	5	cv	$$setvarg$$
14		cmul	$$class\times$$
15	14	cof	$$class{\circ }_f\times$$
16	9	cv	$$setvarq$$
17	13 16 15	co	$$class\left(g{\times }_{f}q\right)$$
18	10 17 12	co	$$class\left(f{-}_f\left(g{\times }_{f}q\right)\right)$$
19		vr	$$setvarr$$
20	19	cv	$$setvarr$$
21	20 6	wceq	$$wffr=0_{𝑝}$$
22		cdgr	$$class\mathrm{deg}$$
23	20 22	cfv	$$class\mathrm{deg}\left(r\right)$$
24		clt	$$class<$$
25	13 22	cfv	$$class\mathrm{deg}\left(g\right)$$
26	23 25 24	wbr	$$wff\mathrm{deg}\left(r\right)<\mathrm{deg}\left(g\right)$$
27	21 26	wo	$$wff\left(r=0_{𝑝}\vee \mathrm{deg}\left(r\right)<\mathrm{deg}\left(g\right)\right)$$
28	27 19 18	wsbc	$$wff\underset{\dot{}}{[}\left(f{-}_f\left(g{\times }_{f}q\right)\right)/r\underset{\dot{}}{]}\left(r=0_{𝑝}\vee \mathrm{deg}\left(r\right)<\mathrm{deg}\left(g\right)\right)$$
29	28 9 4	crio	$$class\left(\iota q\in \mathrm{Poly}\left(ℂ\right)|\underset{\dot{}}{[}\left(f{-}_f\left(g{\times }_{f}q\right)\right)/r\underset{\dot{}}{]}\left(r=0_{𝑝}\vee \mathrm{deg}\left(r\right)<\mathrm{deg}\left(g\right)\right)\right)$$
30	1 5 4 8 29	cmpo	$$class\left(f\in \mathrm{Poly}\left(ℂ\right),g\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{0_{𝑝}\right\}\right)⟼\left(\iota q\in \mathrm{Poly}\left(ℂ\right)|\underset{\dot{}}{[}\left(f{-}_f\left(g{\times }_{f}q\right)\right)/r\underset{\dot{}}{]}\left(r=0_{𝑝}\vee \mathrm{deg}\left(r\right)<\mathrm{deg}\left(g\right)\right)\right)\right)$$
31	0 30	wceq	$$wff\mathrm{quot}=\left(f\in \mathrm{Poly}\left(ℂ\right),g\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{0_{𝑝}\right\}\right)⟼\left(\iota q\in \mathrm{Poly}\left(ℂ\right)|\underset{\dot{}}{[}\left(f{-}_f\left(g{\times }_{f}q\right)\right)/r\underset{\dot{}}{]}\left(r=0_{𝑝}\vee \mathrm{deg}\left(r\right)<\mathrm{deg}\left(g\right)\right)\right)\right)$$