MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-quot Unicode version

Definition df-quot 20161
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 )  \  { 0 p } )  |->  ( iota_ q  e.  (Poly `  CC ) [. ( f  o F  -  ( g  o F  x.  q
) )  /  r ]. ( r  =  0 p  \/  (deg `  r )  <  (deg `  g ) ) ) )
Distinct variable group:    f, g, q, r

Detailed syntax breakdown of Definition df-quot
StepHypRef Expression
1 cquot 20160 . 2  class quot
2 vf . . 3  set  f
3 vg . . 3  set  g
4 cc 8944 . . . 4  class  CC
5 cply 20056 . . . 4  class Poly
64, 5cfv 5413 . . 3  class  (Poly `  CC )
7 c0p 19514 . . . . 5  class  0 p
87csn 3774 . . . 4  class  { 0 p }
96, 8cdif 3277 . . 3  class  ( (Poly `  CC )  \  {
0 p } )
10 vr . . . . . . . 8  set  r
1110cv 1648 . . . . . . 7  class  r
1211, 7wceq 1649 . . . . . 6  wff  r  =  0 p
13 cdgr 20059 . . . . . . . 8  class deg
1411, 13cfv 5413 . . . . . . 7  class  (deg `  r )
153cv 1648 . . . . . . . 8  class  g
1615, 13cfv 5413 . . . . . . 7  class  (deg `  g )
17 clt 9076 . . . . . . 7  class  <
1814, 16, 17wbr 4172 . . . . . 6  wff  (deg `  r )  <  (deg `  g )
1912, 18wo 358 . . . . 5  wff  ( r  =  0 p  \/  (deg `  r )  < 
(deg `  g )
)
202cv 1648 . . . . . 6  class  f
21 vq . . . . . . . 8  set  q
2221cv 1648 . . . . . . 7  class  q
23 cmul 8951 . . . . . . . 8  class  x.
2423cof 6262 . . . . . . 7  class  o F  x.
2515, 22, 24co 6040 . . . . . 6  class  ( g  o F  x.  q
)
26 cmin 9247 . . . . . . 7  class  -
2726cof 6262 . . . . . 6  class  o F  -
2820, 25, 27co 6040 . . . . 5  class  ( f  o F  -  (
g  o F  x.  q ) )
2919, 10, 28wsbc 3121 . . . 4  wff  [. (
f  o F  -  ( g  o F  x.  q ) )  /  r ]. (
r  =  0 p  \/  (deg `  r
)  <  (deg `  g
) )
3029, 21, 6crio 6501 . . 3  class  ( iota_ q  e.  (Poly `  CC ) [. ( f  o F  -  ( g  o F  x.  q
) )  /  r ]. ( r  =  0 p  \/  (deg `  r )  <  (deg `  g ) ) )
312, 3, 6, 9, 30cmpt2 6042 . 2  class  ( f  e.  (Poly `  CC ) ,  g  e.  ( (Poly `  CC )  \  { 0 p }
)  |->  ( iota_ q  e.  (Poly `  CC ) [. ( f  o F  -  ( g  o F  x.  q ) )  /  r ]. ( r  =  0 p  \/  (deg `  r )  <  (deg `  g ) ) ) )
321, 31wceq 1649 1  wff quot  =  ( f  e.  (Poly `  CC ) ,  g  e.  ( (Poly `  CC )  \  { 0 p } )  |->  ( iota_ q  e.  (Poly `  CC ) [. ( f  o F  -  ( g  o F  x.  q
) )  /  r ]. ( r  =  0 p  \/  (deg `  r )  <  (deg `  g ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  quotval  20162
  Copyright terms: Public domain W3C validator