Metamath Proof Explorer


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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cquot
 |-  quot
1 vf
 |-  f
2 cply
 |-  Poly
3 cc
 |-  CC
4 3 2 cfv
 |-  ( Poly ` CC )
5 vg
 |-  g
6 c0p
 |-  0p
7 6 csn
 |-  { 0p }
8 4 7 cdif
 |-  ( ( Poly ` CC ) \ { 0p } )
9 vq
 |-  q
10 1 cv
 |-  f
11 cmin
 |-  -
12 11 cof
 |-  oF -
13 5 cv
 |-  g
14 cmul
 |-  x.
15 14 cof
 |-  oF x.
16 9 cv
 |-  q
17 13 16 15 co
 |-  ( g oF x. q )
18 10 17 12 co
 |-  ( f oF - ( g oF x. q ) )
19 vr
 |-  r
20 19 cv
 |-  r
21 20 6 wceq
 |-  r = 0p
22 cdgr
 |-  deg
23 20 22 cfv
 |-  ( deg ` r )
24 clt
 |-  <
25 13 22 cfv
 |-  ( deg ` g )
26 23 25 24 wbr
 |-  ( deg ` r ) < ( deg ` g )
27 21 26 wo
 |-  ( r = 0p \/ ( deg ` r ) < ( deg ` g ) )
28 27 19 18 wsbc
 |-  [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) )
29 28 9 4 crio
 |-  ( iota_ q e. ( Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) )
30 1 5 4 8 29 cmpo
 |-  ( 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 ) ) ) )
31 0 30 wceq
 |-  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 ) ) ) )