Definition df-q1p 26181

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26186. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20393. (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

Step	Hyp	Ref	Expression
1		cq1p 26176	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3453	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1558	. . . . 5 class 𝑟
6		cpl1 22227	. . . . 5 class Poly1
7	5, 6	cfv 6516	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1558	. . . . . 6 class 𝑝
10		cbs 17236	. . . . . 6 class Base
11	9, 10	cfv 6516	. . . . 5 class (Base‘𝑝)
12		vf	. . . . . 6 setvar 𝑓
13		vg	. . . . . 6 setvar 𝑔
14	8	cv 1558	. . . . . 6 class 𝑏
15	12	cv 1558	. . . . . . . . . 10 class 𝑓
16		vq	. . . . . . . . . . . 12 setvar 𝑞
17	16	cv 1558	. . . . . . . . . . 11 class 𝑞
18	13	cv 1558	. . . . . . . . . . 11 class 𝑔
19		cmulr 17278	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6516	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7391	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18968	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6516	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7391	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 26102	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6516	. . . . . . . . 9 class (deg1‘𝑟)
27	24, 26	cfv 6516	. . . . . . . 8 class ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6516	. . . . . . . 8 class ((deg1‘𝑟)‘𝑔)
29		clt 11210	. . . . . . . 8 class <
30	27, 28, 29	wbr 5097	. . . . . . 7 wff ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)
31	30, 16, 14	crio 7347	. . . . . 6 class (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7393	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3850	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3850	. . 3 class ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
35	2, 3, 34	cmpt 5178	. 2 class (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))
36	1, 35	wceq 1559	1 wff quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))

This definition is referenced by:  q1pval  26203