Definition df-q1p 26090

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26095. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20317. (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 26085	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3459	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1539	. . . . 5 class 𝑟
6		cpl1 22112	. . . . 5 class Poly1
7	5, 6	cfv 6531	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1539	. . . . . 6 class 𝑝
10		cbs 17228	. . . . . 6 class Base
11	9, 10	cfv 6531	. . . . 5 class (Base‘𝑝)
12		vf	. . . . . 6 setvar 𝑓
13		vg	. . . . . 6 setvar 𝑔
14	8	cv 1539	. . . . . 6 class 𝑏
15	12	cv 1539	. . . . . . . . . 10 class 𝑓
16		vq	. . . . . . . . . . . 12 setvar 𝑞
17	16	cv 1539	. . . . . . . . . . 11 class 𝑞
18	13	cv 1539	. . . . . . . . . . 11 class 𝑔
19		cmulr 17272	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6531	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7405	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18918	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6531	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7405	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 26011	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6531	. . . . . . . . 9 class (deg1‘𝑟)
27	24, 26	cfv 6531	. . . . . . . 8 class ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6531	. . . . . . . 8 class ((deg1‘𝑟)‘𝑔)
29		clt 11269	. . . . . . . 8 class <
30	27, 28, 29	wbr 5119	. . . . . . 7 wff ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)
31	30, 16, 14	crio 7361	. . . . . 6 class (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7407	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3874	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3874	. . 3 class ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))
35	2, 3, 34	cmpt 5201	. 2 class (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))
36	1, 35	wceq 1540	1 wff quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))

This definition is referenced by:  q1pval  26112