Definition df-quot 24046

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.)

Assertion

Ref	Expression
df-quot	|- quot = ( f e. (Poly ` CC ) , g e. ( (Poly ` CC ) \ { 0p } ) |-> ( iota_ q e. (Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ (deg ` r ) < (deg ` g ) ) ) )

Distinct variable group:   f, g, q, r

Detailed syntax breakdown of Definition df-quot

Step	Hyp	Ref	Expression
1		cquot 24045	. 2 class quot
2		vf	. . 3 setvar f
3		vg	. . 3 setvar g
4		cc 9934	. . . 4 class CC
5		cply 23940	. . . 4 class Poly
6	4, 5	cfv 5888	. . 3 class (Poly ` CC )
7		c0p 23436	. . . . 5 class 0p
8	7	csn 4177	. . . 4 class { 0p }
9	6, 8	cdif 3571	. . 3 class ( (Poly ` CC ) \ { 0p } )
10		vr	. . . . . . . 8 setvar r
11	10	cv 1482	. . . . . . 7 class r
12	11, 7	wceq 1483	. . . . . 6 wff r = 0p
13		cdgr 23943	. . . . . . . 8 class deg
14	11, 13	cfv 5888	. . . . . . 7 class (deg ` r )
15	3	cv 1482	. . . . . . . 8 class g
16	15, 13	cfv 5888	. . . . . . 7 class (deg ` g )
17		clt 10074	. . . . . . 7 class <
18	14, 16, 17	wbr 4653	. . . . . 6 wff (deg ` r ) < (deg ` g )
19	12, 18	wo 383	. . . . 5 wff ( r = 0p \/ (deg ` r ) < (deg ` g ) )
20	2	cv 1482	. . . . . 6 class f
21		vq	. . . . . . . 8 setvar q
22	21	cv 1482	. . . . . . 7 class q
23		cmul 9941	. . . . . . . 8 class x.
24	23	cof 6895	. . . . . . 7 class oF x.
25	15, 22, 24	co 6650	. . . . . 6 class ( g oF x. q )
26		cmin 10266	. . . . . . 7 class -
27	26	cof 6895	. . . . . 6 class oF -
28	20, 25, 27	co 6650	. . . . 5 class ( f oF - ( g oF x. q ) )
29	19, 10, 28	wsbc 3435	. . . 4 wff [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ (deg ` r ) < (deg ` g ) )
30	29, 21, 6	crio 6610	. . 3 class ( iota_ q e. (Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ (deg ` r ) < (deg ` g ) ) )
31	2, 3, 6, 9, 30	cmpt2 6652	. 2 class ( f e. (Poly ` CC ) , g e. ( (Poly ` CC ) \ { 0p } ) |-> ( iota_ q e. (Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ (deg ` r ) < (deg ` g ) ) ) )
32	1, 31	wceq 1483	1 wff quot = ( f e. (Poly ` CC ) , g e. ( (Poly ` CC ) \ { 0p } ) |-> ( iota_ q e. (Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ (deg ` r ) < (deg ` g ) ) ) )

This definition is referenced by:  quotval  24047