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 24233
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 24238. We actually use the reversed version for better harmony with our divisibility df-dvdsr 18957. (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 24228 . 2 class quot1p
2 vr . . 3 setvar 𝑟
3 cvv 3385 . . 3 class V
4 vp . . . 4 setvar 𝑝
52cv 1652 . . . . 5 class 𝑟
6 cpl1 19869 . . . . 5 class Poly1
75, 6cfv 6101 . . . 4 class (Poly1𝑟)
8 vb . . . . 5 setvar 𝑏
94cv 1652 . . . . . 6 class 𝑝
10 cbs 16184 . . . . . 6 class Base
119, 10cfv 6101 . . . . 5 class (Base‘𝑝)
12 vf . . . . . 6 setvar 𝑓
13 vg . . . . . 6 setvar 𝑔
148cv 1652 . . . . . 6 class 𝑏
1512cv 1652 . . . . . . . . . 10 class 𝑓
16 vq . . . . . . . . . . . 12 setvar 𝑞
1716cv 1652 . . . . . . . . . . 11 class 𝑞
1813cv 1652 . . . . . . . . . . 11 class 𝑔
19 cmulr 16268 . . . . . . . . . . . 12 class .r
209, 19cfv 6101 . . . . . . . . . . 11 class (.r𝑝)
2117, 18, 20co 6878 . . . . . . . . . 10 class (𝑞(.r𝑝)𝑔)
22 csg 17740 . . . . . . . . . . 11 class -g
239, 22cfv 6101 . . . . . . . . . 10 class (-g𝑝)
2415, 21, 23co 6878 . . . . . . . . 9 class (𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))
25 cdg1 24155 . . . . . . . . . 10 class deg1
265, 25cfv 6101 . . . . . . . . 9 class ( deg1𝑟)
2724, 26cfv 6101 . . . . . . . 8 class (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔)))
2818, 26cfv 6101 . . . . . . . 8 class (( deg1𝑟)‘𝑔)
29 clt 10363 . . . . . . . 8 class <
3027, 28, 29wbr 4843 . . . . . . 7 wff (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)
3130, 16, 14crio 6838 . . . . . 6 class (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))
3212, 13, 14, 14, 31cmpt2 6880 . . . . 5 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
338, 11, 32csb 3728 . . . 4 class (Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
344, 7, 33csb 3728 . . 3 class (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
352, 3, 34cmpt 4922 . 2 class (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
361, 35wceq 1653 1 wff quot1p = (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  q1pval  24254
  Copyright terms: Public domain W3C validator