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

Definition df-r1p 23874
 Description: Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-r1p rem1p = (𝑟 ∈ V ↦ (Base‘(Poly1𝑟)) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔))))
Distinct variable group:   𝑓,𝑟,𝑔,𝑏

Detailed syntax breakdown of Definition df-r1p
StepHypRef Expression
1 cr1p 23869 . 2 class rem1p
2 vr . . 3 setvar 𝑟
3 cvv 3195 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1480 . . . . . 6 class 𝑟
6 cpl1 19528 . . . . . 6 class Poly1
75, 6cfv 5876 . . . . 5 class (Poly1𝑟)
8 cbs 15838 . . . . 5 class Base
97, 8cfv 5876 . . . 4 class (Base‘(Poly1𝑟))
10 vf . . . . 5 setvar 𝑓
11 vg . . . . 5 setvar 𝑔
124cv 1480 . . . . 5 class 𝑏
1310cv 1480 . . . . . 6 class 𝑓
1411cv 1480 . . . . . . . 8 class 𝑔
15 cq1p 23868 . . . . . . . . 9 class quot1p
165, 15cfv 5876 . . . . . . . 8 class (quot1p𝑟)
1713, 14, 16co 6635 . . . . . . 7 class (𝑓(quot1p𝑟)𝑔)
18 cmulr 15923 . . . . . . . 8 class .r
197, 18cfv 5876 . . . . . . 7 class (.r‘(Poly1𝑟))
2017, 14, 19co 6635 . . . . . 6 class ((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔)
21 csg 17405 . . . . . . 7 class -g
227, 21cfv 5876 . . . . . 6 class (-g‘(Poly1𝑟))
2313, 20, 22co 6635 . . . . 5 class (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔))
2410, 11, 12, 12, 23cmpt2 6637 . . . 4 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔)))
254, 9, 24csb 3526 . . 3 class (Base‘(Poly1𝑟)) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔)))
262, 3, 25cmpt 4720 . 2 class (𝑟 ∈ V ↦ (Base‘(Poly1𝑟)) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔))))
271, 26wceq 1481 1 wff rem1p = (𝑟 ∈ V ↦ (Base‘(Poly1𝑟)) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔))))
 Colors of variables: wff setvar class This definition is referenced by:  r1pval  23897
 Copyright terms: Public domain W3C validator