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

Definition df-q1p 26157
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26162. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20335. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-q1p quot1p = (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔))))
Distinct variable group:   𝑓,𝑟,𝑔,𝑏,𝑝,𝑞

Detailed syntax breakdown of Definition df-q1p
StepHypRef Expression
1 cq1p 26152 . 2 class quot1p
2 vr . . 3 setvar 𝑟
3 cvv 3462 . . 3 class V
4 vp . . . 4 setvar 𝑝
52cv 1533 . . . . 5 class 𝑟
6 cpl1 22162 . . . . 5 class Poly1
75, 6cfv 6546 . . . 4 class (Poly1𝑟)
8 vb . . . . 5 setvar 𝑏
94cv 1533 . . . . . 6 class 𝑝
10 cbs 17208 . . . . . 6 class Base
119, 10cfv 6546 . . . . 5 class (Base‘𝑝)
12 vf . . . . . 6 setvar 𝑓
13 vg . . . . . 6 setvar 𝑔
148cv 1533 . . . . . 6 class 𝑏
1512cv 1533 . . . . . . . . . 10 class 𝑓
16 vq . . . . . . . . . . . 12 setvar 𝑞
1716cv 1533 . . . . . . . . . . 11 class 𝑞
1813cv 1533 . . . . . . . . . . 11 class 𝑔
19 cmulr 17262 . . . . . . . . . . . 12 class .r
209, 19cfv 6546 . . . . . . . . . . 11 class (.r𝑝)
2117, 18, 20co 7416 . . . . . . . . . 10 class (𝑞(.r𝑝)𝑔)
22 csg 18925 . . . . . . . . . . 11 class -g
239, 22cfv 6546 . . . . . . . . . 10 class (-g𝑝)
2415, 21, 23co 7416 . . . . . . . . 9 class (𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))
25 cdg1 26075 . . . . . . . . . 10 class deg1
265, 25cfv 6546 . . . . . . . . 9 class (deg1𝑟)
2724, 26cfv 6546 . . . . . . . 8 class ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔)))
2818, 26cfv 6546 . . . . . . . 8 class ((deg1𝑟)‘𝑔)
29 clt 11289 . . . . . . . 8 class <
3027, 28, 29wbr 5145 . . . . . . 7 wff ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)
3130, 16, 14crio 7371 . . . . . 6 class (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔))
3212, 13, 14, 14, 31cmpo 7418 . . . . 5 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)))
338, 11, 32csb 3891 . . . 4 class (Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)))
344, 7, 33csb 3891 . . 3 class (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)))
352, 3, 34cmpt 5228 . 2 class (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔))))
361, 35wceq 1534 1 wff quot1p = (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  q1pval  26179
  Copyright terms: Public domain W3C validator