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

Definition df-r1p 19519
Description: Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-r1p  |- rem1p  =  (
r  e.  _V  |->  [_ ( Base `  (Poly1 `  r
) )  /  b ]_ ( f  e.  b ,  g  e.  b 
|->  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r ) g ) ( .r `  (Poly1 `  r ) ) g ) ) ) )
Distinct variable group:    f, r, g, b

Detailed syntax breakdown of Definition df-r1p
StepHypRef Expression
1 cr1p 19514 . 2  class rem1p
2 vr . . 3  set  r
3 cvv 2788 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1622 . . . . . 6  class  r
6 cpl1 16252 . . . . . 6  class Poly1
75, 6cfv 5255 . . . . 5  class  (Poly1 `  r
)
8 cbs 13148 . . . . 5  class  Base
97, 8cfv 5255 . . . 4  class  ( Base `  (Poly1 `  r ) )
10 vf . . . . 5  set  f
11 vg . . . . 5  set  g
124cv 1622 . . . . 5  class  b
1310cv 1622 . . . . . 6  class  f
1411cv 1622 . . . . . . . 8  class  g
15 cq1p 19513 . . . . . . . . 9  class quot1p
165, 15cfv 5255 . . . . . . . 8  class  (quot1p `  r
)
1713, 14, 16co 5858 . . . . . . 7  class  ( f (quot1p `  r ) g )
18 cmulr 13209 . . . . . . . 8  class  .r
197, 18cfv 5255 . . . . . . 7  class  ( .r
`  (Poly1 `  r ) )
2017, 14, 19co 5858 . . . . . 6  class  ( ( f (quot1p `  r ) g ) ( .r `  (Poly1 `  r ) ) g )
21 csg 14365 . . . . . . 7  class  -g
227, 21cfv 5255 . . . . . 6  class  ( -g `  (Poly1 `  r ) )
2313, 20, 22co 5858 . . . . 5  class  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r
) g ) ( .r `  (Poly1 `  r
) ) g ) )
2410, 11, 12, 12, 23cmpt2 5860 . . . 4  class  ( f  e.  b ,  g  e.  b  |->  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r
) g ) ( .r `  (Poly1 `  r
) ) g ) ) )
254, 9, 24csb 3081 . . 3  class  [_ ( Base `  (Poly1 `  r ) )  /  b ]_ (
f  e.  b ,  g  e.  b  |->  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r
) g ) ( .r `  (Poly1 `  r
) ) g ) ) )
262, 3, 25cmpt 4077 . 2  class  ( r  e.  _V  |->  [_ ( Base `  (Poly1 `  r ) )  /  b ]_ (
f  e.  b ,  g  e.  b  |->  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r
) g ) ( .r `  (Poly1 `  r
) ) g ) ) ) )
271, 26wceq 1623 1  wff rem1p  =  (
r  e.  _V  |->  [_ ( Base `  (Poly1 `  r
) )  /  b ]_ ( f  e.  b ,  g  e.  b 
|->  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r ) g ) ( .r `  (Poly1 `  r ) ) g ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  r1pval  19542
  Copyright terms: Public domain W3C validator