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 23937
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 23942. We actually use the reversed version for better harmony with our divisibility df-dvdsr 18687. (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 23932 . 2 class quot1p
2 vr . . 3 setvar 𝑟
3 cvv 3231 . . 3 class V
4 vp . . . 4 setvar 𝑝
52cv 1522 . . . . 5 class 𝑟
6 cpl1 19595 . . . . 5 class Poly1
75, 6cfv 5926 . . . 4 class (Poly1𝑟)
8 vb . . . . 5 setvar 𝑏
94cv 1522 . . . . . 6 class 𝑝
10 cbs 15904 . . . . . 6 class Base
119, 10cfv 5926 . . . . 5 class (Base‘𝑝)
12 vf . . . . . 6 setvar 𝑓
13 vg . . . . . 6 setvar 𝑔
148cv 1522 . . . . . 6 class 𝑏
1512cv 1522 . . . . . . . . . 10 class 𝑓
16 vq . . . . . . . . . . . 12 setvar 𝑞
1716cv 1522 . . . . . . . . . . 11 class 𝑞
1813cv 1522 . . . . . . . . . . 11 class 𝑔
19 cmulr 15989 . . . . . . . . . . . 12 class .r
209, 19cfv 5926 . . . . . . . . . . 11 class (.r𝑝)
2117, 18, 20co 6690 . . . . . . . . . 10 class (𝑞(.r𝑝)𝑔)
22 csg 17471 . . . . . . . . . . 11 class -g
239, 22cfv 5926 . . . . . . . . . 10 class (-g𝑝)
2415, 21, 23co 6690 . . . . . . . . 9 class (𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))
25 cdg1 23859 . . . . . . . . . 10 class deg1
265, 25cfv 5926 . . . . . . . . 9 class ( deg1𝑟)
2724, 26cfv 5926 . . . . . . . 8 class (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔)))
2818, 26cfv 5926 . . . . . . . 8 class (( deg1𝑟)‘𝑔)
29 clt 10112 . . . . . . . 8 class <
3027, 28, 29wbr 4685 . . . . . . 7 wff (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)
3130, 16, 14crio 6650 . . . . . 6 class (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))
3212, 13, 14, 14, 31cmpt2 6692 . . . . 5 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
338, 11, 32csb 3566 . . . 4 class (Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
344, 7, 33csb 3566 . . 3 class (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔)))
352, 3, 34cmpt 4762 . 2 class (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
361, 35wceq 1523 1 wff quot1p = (𝑟 ∈ V ↦ (Poly1𝑟) / 𝑝(Base‘𝑝) / 𝑏(𝑓𝑏, 𝑔𝑏 ↦ (𝑞𝑏 (( deg1𝑟)‘(𝑓(-g𝑝)(𝑞(.r𝑝)𝑔))) < (( deg1𝑟)‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  q1pval  23958
  Copyright terms: Public domain W3C validator