Definition df-q1p 26506

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26511. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20638. (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 26501	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3454	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1569	. . . . 5 class 𝑟
6		cpl1 22550	. . . . 5 class Poly1
7	5, 6	cfv 6566	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1569	. . . . . 6 class 𝑝
10		cbs 17431	. . . . . 6 class Base
11	9, 10	cfv 6566	. . . . 5 class (Base‘𝑝)
12		vf	. . . . . 6 setvar 𝑓
13		vg	. . . . . 6 setvar 𝑔
14	8	cv 1569	. . . . . 6 class 𝑏
15	12	cv 1569	. . . . . . . . . 10 class 𝑓
16		vq	. . . . . . . . . . . 12 setvar 𝑞
17	16	cv 1569	. . . . . . . . . . 11 class 𝑞
18	13	cv 1569	. . . . . . . . . . 11 class 𝑔
19		cmulr 17473	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6566	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7451	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 19196	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6566	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7451	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 26427	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6566	. . . . . . . . 9 class (deg1‘𝑟)
27	24, 26	cfv 6566	. . . . . . . 8 class ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6566	. . . . . . . 8 class ((deg1‘𝑟)‘𝑔)
29		clt 11382	. . . . . . . 8 class <
30	27, 28, 29	wbr 5108	. . . . . . 7 wff ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)
31	30, 16, 14	crio 7407	. . . . . 6 class (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7453	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3851	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3851	. . 3 class ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
35	2, 3, 34	cmpt 5192	. 2 class (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))
36	1, 35	wceq 1570	1 wff quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))

This definition is used by:  q1pval  26528