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

Definition df-quot 19687
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 19686 . 2  class quot
2 vf . . 3  set  f
3 vg . . 3  set  g
4 cc 8751 . . . 4  class  CC
5 cply 19582 . . . 4  class Poly
64, 5cfv 5271 . . 3  class  (Poly `  CC )
7 c0p 19040 . . . . 5  class  0 p
87csn 3653 . . . 4  class  { 0 p }
96, 8cdif 3162 . . 3  class  ( (Poly `  CC )  \  {
0 p } )
10 vr . . . . . . . 8  set  r
1110cv 1631 . . . . . . 7  class  r
1211, 7wceq 1632 . . . . . 6  wff  r  =  0 p
13 cdgr 19585 . . . . . . . 8  class deg
1411, 13cfv 5271 . . . . . . 7  class  (deg `  r )
153cv 1631 . . . . . . . 8  class  g
1615, 13cfv 5271 . . . . . . 7  class  (deg `  g )
17 clt 8883 . . . . . . 7  class  <
1814, 16, 17wbr 4039 . . . . . 6  wff  (deg `  r )  <  (deg `  g )
1912, 18wo 357 . . . . 5  wff  ( r  =  0 p  \/  (deg `  r )  < 
(deg `  g )
)
202cv 1631 . . . . . 6  class  f
21 vq . . . . . . . 8  set  q
2221cv 1631 . . . . . . 7  class  q
23 cmul 8758 . . . . . . . 8  class  x.
2423cof 6092 . . . . . . 7  class  o F  x.
2515, 22, 24co 5874 . . . . . 6  class  ( g  o F  x.  q
)
26 cmin 9053 . . . . . . 7  class  -
2726cof 6092 . . . . . 6  class  o F  -
2820, 25, 27co 5874 . . . . 5  class  ( f  o F  -  (
g  o F  x.  q ) )
2919, 10, 28wsbc 3004 . . . 4  wff  [. (
f  o F  -  ( g  o F  x.  q ) )  /  r ]. (
r  =  0 p  \/  (deg `  r
)  <  (deg `  g
) )
3029, 21, 6crio 6313 . . 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 5876 . 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 1632 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  19688
  Copyright terms: Public domain W3C validator