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

Definition df-r1p 24732
 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 24727 . 2 class rem1p
2 vr . . 3 setvar 𝑟
3 cvv 3480 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1537 . . . . . 6 class 𝑟
6 cpl1 20340 . . . . . 6 class Poly1
75, 6cfv 6344 . . . . 5 class (Poly1𝑟)
8 cbs 16481 . . . . 5 class Base
97, 8cfv 6344 . . . 4 class (Base‘(Poly1𝑟))
10 vf . . . . 5 setvar 𝑓
11 vg . . . . 5 setvar 𝑔
124cv 1537 . . . . 5 class 𝑏
1310cv 1537 . . . . . 6 class 𝑓
1411cv 1537 . . . . . . . 8 class 𝑔
15 cq1p 24726 . . . . . . . . 9 class quot1p
165, 15cfv 6344 . . . . . . . 8 class (quot1p𝑟)
1713, 14, 16co 7146 . . . . . . 7 class (𝑓(quot1p𝑟)𝑔)
18 cmulr 16564 . . . . . . . 8 class .r
197, 18cfv 6344 . . . . . . 7 class (.r‘(Poly1𝑟))
2017, 14, 19co 7146 . . . . . 6 class ((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔)
21 csg 18103 . . . . . . 7 class -g
227, 21cfv 6344 . . . . . 6 class (-g‘(Poly1𝑟))
2313, 20, 22co 7146 . . . . 5 class (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔))
2410, 11, 12, 12, 23cmpo 7148 . . . 4 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔)))
254, 9, 24csb 3866 . . 3 class (Base‘(Poly1𝑟)) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔)))
262, 3, 25cmpt 5133 . 2 class (𝑟 ∈ V ↦ (Base‘(Poly1𝑟)) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔))))
271, 26wceq 1538 1 wff rem1p = (𝑟 ∈ V ↦ (Base‘(Poly1𝑟)) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑓(-g‘(Poly1𝑟))((𝑓(quot1p𝑟)𝑔)(.r‘(Poly1𝑟))𝑔))))
 Colors of variables: wff setvar class This definition is referenced by:  r1pval  24755
 Copyright terms: Public domain W3C validator