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 24653
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 24658. We actually use the reversed version for better harmony with our divisibility df-dvdsr 19320. (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 24648 . 2 class quot1p
2 vr . . 3 setvar 𝑟
3 cvv 3492 . . 3 class V
4 vp . . . 4 setvar 𝑝
52cv 1527 . . . . 5 class 𝑟
6 cpl1 20273 . . . . 5 class Poly1
75, 6cfv 6348 . . . 4 class (Poly1𝑟)
8 vb . . . . 5 setvar 𝑏
94cv 1527 . . . . . 6 class 𝑝
10 cbs 16471 . . . . . 6 class Base
119, 10cfv 6348 . . . . 5 class (Base‘𝑝)
12 vf . . . . . 6 setvar 𝑓
13 vg . . . . . 6 setvar 𝑔
148cv 1527 . . . . . 6 class 𝑏
1512cv 1527 . . . . . . . . . 10 class 𝑓
16 vq . . . . . . . . . . . 12 setvar 𝑞
1716cv 1527 . . . . . . . . . . 11 class 𝑞
1813cv 1527 . . . . . . . . . . 11 class 𝑔
19 cmulr 16554 . . . . . . . . . . . 12 class .r
209, 19cfv 6348 . . . . . . . . . . 11 class (.r𝑝)
2117, 18, 20co 7145 . . . . . . . . . 10 class (𝑞(.r𝑝)𝑔)
22 csg 18043 . . . . . . . . . . 11 class -g
239, 22cfv 6348 . . . . . . . . . 10 class (-g𝑝)
2415, 21, 23co 7145 . . . . . . . . 9 class (𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))
25 cdg1 24575 . . . . . . . . . 10 class deg1
265, 25cfv 6348 . . . . . . . . 9 class ( deg1𝑟)
2724, 26cfv 6348 . . . . . . . 8 class (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔)))
2818, 26cfv 6348 . . . . . . . 8 class (( deg1𝑟)‘𝑔)
29 clt 10663 . . . . . . . 8 class <
3027, 28, 29wbr 5057 . . . . . . 7 wff (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)
3130, 16, 14crio 7102 . . . . . 6 class (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))
3212, 13, 14, 14, 31cmpo 7147 . . . . 5 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
338, 11, 32csb 3880 . . . 4 class (Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
344, 7, 33csb 3880 . . 3 class (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
352, 3, 34cmpt 5137 . 2 class (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
361, 35wceq 1528 1 wff quot1p = (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  q1pval  24674
  Copyright terms: Public domain W3C validator