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

Definition df-quot 21757
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
StepHypRef Expression
1 cquot 21756 . 2  class quot
2 vf . . 3  setvar  f
3 vg . . 3  setvar  g
4 cc 9280 . . . 4  class  CC
5 cply 21652 . . . 4  class Poly
64, 5cfv 5418 . . 3  class  (Poly `  CC )
7 c0p 21147 . . . . 5  class  0p
87csn 3877 . . . 4  class  { 0p }
96, 8cdif 3325 . . 3  class  ( (Poly `  CC )  \  {
0p } )
10 vr . . . . . . . 8  setvar  r
1110cv 1368 . . . . . . 7  class  r
1211, 7wceq 1369 . . . . . 6  wff  r  =  0p
13 cdgr 21655 . . . . . . . 8  class deg
1411, 13cfv 5418 . . . . . . 7  class  (deg `  r )
153cv 1368 . . . . . . . 8  class  g
1615, 13cfv 5418 . . . . . . 7  class  (deg `  g )
17 clt 9418 . . . . . . 7  class  <
1814, 16, 17wbr 4292 . . . . . 6  wff  (deg `  r )  <  (deg `  g )
1912, 18wo 368 . . . . 5  wff  ( r  =  0p  \/  (deg `  r )  <  (deg `  g )
)
202cv 1368 . . . . . 6  class  f
21 vq . . . . . . . 8  setvar  q
2221cv 1368 . . . . . . 7  class  q
23 cmul 9287 . . . . . . . 8  class  x.
2423cof 6318 . . . . . . 7  class  oF  x.
2515, 22, 24co 6091 . . . . . 6  class  ( g  oF  x.  q
)
26 cmin 9595 . . . . . . 7  class  -
2726cof 6318 . . . . . 6  class  oF  -
2820, 25, 27co 6091 . . . . 5  class  ( f  oF  -  (
g  oF  x.  q ) )
2919, 10, 28wsbc 3186 . . . 4  wff  [. (
f  oF  -  ( g  oF  x.  q ) )  /  r ]. (
r  =  0p  \/  (deg `  r
)  <  (deg `  g
) )
3029, 21, 6crio 6051 . . 3  class  ( iota_ q  e.  (Poly `  CC ) [. ( f  oF  -  ( g  oF  x.  q
) )  /  r ]. ( r  =  0p  \/  (deg `  r )  <  (deg `  g ) ) )
312, 3, 6, 9, 30cmpt2 6093 . 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 ) ) ) )
321, 31wceq 1369 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 ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  quotval  21758
  Copyright terms: Public domain W3C validator