Definition df-q1p 26271

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26276. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20440. (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 26266	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3455	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1569	. . . . 5 class 𝑟
6		cpl1 22318	. . . . 5 class Poly1
7	5, 6	cfv 6538	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1569	. . . . . 6 class 𝑝
10		cbs 17270	. . . . . 6 class Base
11	9, 10	cfv 6538	. . . . 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 17312	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6538	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7412	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 19003	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6538	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7412	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 26192	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6538	. . . . . . . . 9 class (deg1‘𝑟)
27	24, 26	cfv 6538	. . . . . . . 8 class ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6538	. . . . . . . 8 class ((deg1‘𝑟)‘𝑔)
29		clt 11244	. . . . . . . 8 class <
30	27, 28, 29	wbr 5110	. . . . . . 7 wff ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)
31	30, 16, 14	crio 7368	. . . . . 6 class (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7414	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3854	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3854	. . 3 class ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
35	2, 3, 34	cmpt 5193	. 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 referenced by:  q1pval  26293