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 26172
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26177. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20357. (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 26167 . 2 class quot1p
2 vr . . 3 setvar 𝑟
3 cvv 3480 . . 3 class V
4 vp . . . 4 setvar 𝑝
52cv 1539 . . . . 5 class 𝑟
6 cpl1 22178 . . . . 5 class Poly1
75, 6cfv 6561 . . . 4 class (Poly1𝑟)
8 vb . . . . 5 setvar 𝑏
94cv 1539 . . . . . 6 class 𝑝
10 cbs 17247 . . . . . 6 class Base
119, 10cfv 6561 . . . . 5 class (Base‘𝑝)
12 vf . . . . . 6 setvar 𝑓
13 vg . . . . . 6 setvar 𝑔
148cv 1539 . . . . . 6 class 𝑏
1512cv 1539 . . . . . . . . . 10 class 𝑓
16 vq . . . . . . . . . . . 12 setvar 𝑞
1716cv 1539 . . . . . . . . . . 11 class 𝑞
1813cv 1539 . . . . . . . . . . 11 class 𝑔
19 cmulr 17298 . . . . . . . . . . . 12 class .r
209, 19cfv 6561 . . . . . . . . . . 11 class (.r𝑝)
2117, 18, 20co 7431 . . . . . . . . . 10 class (𝑞(.r𝑝)𝑔)
22 csg 18953 . . . . . . . . . . 11 class -g
239, 22cfv 6561 . . . . . . . . . 10 class (-g𝑝)
2415, 21, 23co 7431 . . . . . . . . 9 class (𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))
25 cdg1 26093 . . . . . . . . . 10 class deg1
265, 25cfv 6561 . . . . . . . . 9 class (deg1𝑟)
2724, 26cfv 6561 . . . . . . . 8 class ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔)))
2818, 26cfv 6561 . . . . . . . 8 class ((deg1𝑟)‘𝑔)
29 clt 11295 . . . . . . . 8 class <
3027, 28, 29wbr 5143 . . . . . . 7 wff ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)
3130, 16, 14crio 7387 . . . . . 6 class (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔))
3212, 13, 14, 14, 31cmpo 7433 . . . . 5 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)))
338, 11, 32csb 3899 . . . 4 class (Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)))
344, 7, 33csb 3899 . . 3 class (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔)))
352, 3, 34cmpt 5225 . 2 class (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔))))
361, 35wceq 1540 1 wff quot1p = (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 ((deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < ((deg1𝑟)‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  q1pval  26194
  Copyright terms: Public domain W3C validator