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

Definition df-r1p 19572
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 19567 . 2  class rem1p
2 vr . . 3  set  r
3 cvv 2822 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1632 . . . . . 6  class  r
6 cpl1 16301 . . . . . 6  class Poly1
75, 6cfv 5292 . . . . 5  class  (Poly1 `  r
)
8 cbs 13195 . . . . 5  class  Base
97, 8cfv 5292 . . . 4  class  ( Base `  (Poly1 `  r ) )
10 vf . . . . 5  set  f
11 vg . . . . 5  set  g
124cv 1632 . . . . 5  class  b
1310cv 1632 . . . . . 6  class  f
1411cv 1632 . . . . . . . 8  class  g
15 cq1p 19566 . . . . . . . . 9  class quot1p
165, 15cfv 5292 . . . . . . . 8  class  (quot1p `  r
)
1713, 14, 16co 5900 . . . . . . 7  class  ( f (quot1p `  r ) g )
18 cmulr 13256 . . . . . . . 8  class  .r
197, 18cfv 5292 . . . . . . 7  class  ( .r
`  (Poly1 `  r ) )
2017, 14, 19co 5900 . . . . . 6  class  ( ( f (quot1p `  r ) g ) ( .r `  (Poly1 `  r ) ) g )
21 csg 14414 . . . . . . 7  class  -g
227, 21cfv 5292 . . . . . 6  class  ( -g `  (Poly1 `  r ) )
2313, 20, 22co 5900 . . . . 5  class  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r
) g ) ( .r `  (Poly1 `  r
) ) g ) )
2410, 11, 12, 12, 23cmpt2 5902 . . . 4  class  ( f  e.  b ,  g  e.  b  |->  ( f ( -g `  (Poly1 `  r ) ) ( ( f (quot1p `  r
) g ) ( .r `  (Poly1 `  r
) ) g ) ) )
254, 9, 24csb 3115 . . 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 4114 . 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 1633 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  19595
  Copyright terms: Public domain W3C validator