Definition df-q1p 25884

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 25889. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20250. (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 25879	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3472	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1538	. . . . 5 class 𝑟
6		cpl1 21922	. . . . 5 class Poly1
7	5, 6	cfv 6544	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1538	. . . . . 6 class 𝑝
10		cbs 17150	. . . . . 6 class Base
11	9, 10	cfv 6544	. . . . 5 class (Base‘𝑝)
12		vf	. . . . . 6 setvar 𝑓
13		vg	. . . . . 6 setvar 𝑔
14	8	cv 1538	. . . . . 6 class 𝑏
15	12	cv 1538	. . . . . . . . . 10 class 𝑓
16		vq	. . . . . . . . . . . 12 setvar 𝑞
17	16	cv 1538	. . . . . . . . . . 11 class 𝑞
18	13	cv 1538	. . . . . . . . . . 11 class 𝑔
19		cmulr 17204	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6544	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7413	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18859	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6544	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7413	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 25803	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6544	. . . . . . . . 9 class ( deg1 ‘𝑟)
27	24, 26	cfv 6544	. . . . . . . 8 class (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6544	. . . . . . . 8 class (( deg1 ‘𝑟)‘𝑔)
29		clt 11254	. . . . . . . 8 class <
30	27, 28, 29	wbr 5149	. . . . . . 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 7415	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3894	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3894	. . 3 class ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
35	2, 3, 34	cmpt 5232	. 2 class (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))))
36	1, 35	wceq 1539	1 wff quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))))

This definition is referenced by:  q1pval  25905