This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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