Definition df-q1p 25534

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 25539. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20084. (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 25529	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3446	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1540	. . . . 5 class 𝑟
6		cpl1 21585	. . . . 5 class Poly1
7	5, 6	cfv 6501	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1540	. . . . . 6 class 𝑝
10		cbs 17094	. . . . . 6 class Base
11	9, 10	cfv 6501	. . . . 5 class (Base‘𝑝)
12		vf	. . . . . 6 setvar 𝑓
13		vg	. . . . . 6 setvar 𝑔
14	8	cv 1540	. . . . . 6 class 𝑏
15	12	cv 1540	. . . . . . . . . 10 class 𝑓
16		vq	. . . . . . . . . . . 12 setvar 𝑞
17	16	cv 1540	. . . . . . . . . . 11 class 𝑞
18	13	cv 1540	. . . . . . . . . . 11 class 𝑔
19		cmulr 17148	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6501	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7362	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18764	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6501	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7362	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 25453	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6501	. . . . . . . . 9 class ( deg1 ‘𝑟)
27	24, 26	cfv 6501	. . . . . . . 8 class (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6501	. . . . . . . 8 class (( deg1 ‘𝑟)‘𝑔)
29		clt 11198	. . . . . . . 8 class <
30	27, 28, 29	wbr 5110	. . . . . . 7 wff (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)
31	30, 16, 14	crio 7317	. . . . . 6 class (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7364	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3858	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3858	. . 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 1541	1 wff quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))))

This definition is referenced by:  q1pval  25555