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 24712
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 24717. We actually use the reversed version for better harmony with our divisibility df-dvdsr 19370. (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 24707 . 2 class quot1p
2 vr . . 3 setvar 𝑟
3 cvv 3473 . . 3 class V
4 vp . . . 4 setvar 𝑝
52cv 1536 . . . . 5 class 𝑟
6 cpl1 20321 . . . . 5 class Poly1
75, 6cfv 6331 . . . 4 class (Poly1𝑟)
8 vb . . . . 5 setvar 𝑏
94cv 1536 . . . . . 6 class 𝑝
10 cbs 16462 . . . . . 6 class Base
119, 10cfv 6331 . . . . 5 class (Base‘𝑝)
12 vf . . . . . 6 setvar 𝑓
13 vg . . . . . 6 setvar 𝑔
148cv 1536 . . . . . 6 class 𝑏
1512cv 1536 . . . . . . . . . 10 class 𝑓
16 vq . . . . . . . . . . . 12 setvar 𝑞
1716cv 1536 . . . . . . . . . . 11 class 𝑞
1813cv 1536 . . . . . . . . . . 11 class 𝑔
19 cmulr 16545 . . . . . . . . . . . 12 class .r
209, 19cfv 6331 . . . . . . . . . . 11 class (.r𝑝)
2117, 18, 20co 7133 . . . . . . . . . 10 class (𝑞(.r𝑝)𝑔)
22 csg 18084 . . . . . . . . . . 11 class -g
239, 22cfv 6331 . . . . . . . . . 10 class (-g𝑝)
2415, 21, 23co 7133 . . . . . . . . 9 class (𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))
25 cdg1 24634 . . . . . . . . . 10 class deg1
265, 25cfv 6331 . . . . . . . . 9 class ( deg1𝑟)
2724, 26cfv 6331 . . . . . . . 8 class (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔)))
2818, 26cfv 6331 . . . . . . . 8 class (( deg1𝑟)‘𝑔)
29 clt 10653 . . . . . . . 8 class <
3027, 28, 29wbr 5042 . . . . . . 7 wff (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)
3130, 16, 14crio 7090 . . . . . 6 class (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))
3212, 13, 14, 14, 31cmpo 7135 . . . . 5 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
338, 11, 32csb 3860 . . . 4 class (Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
344, 7, 33csb 3860 . . 3 class (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
352, 3, 34cmpt 5122 . 2 class (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
361, 35wceq 1537 1 wff quot1p = (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  q1pval  24733
  Copyright terms: Public domain W3C validator