Definition df-q1p 25650

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 25655. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20171. (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 25645	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3475	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1541	. . . . 5 class 𝑟
6		cpl1 21701	. . . . 5 class Poly1
7	5, 6	cfv 6544	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1541	. . . . . 6 class 𝑝
10		cbs 17144	. . . . . 6 class Base
11	9, 10	cfv 6544	. . . . 5 class (Base‘𝑝)
12		vf	. . . . . 6 setvar 𝑓
13		vg	. . . . . 6 setvar 𝑔
14	8	cv 1541	. . . . . 6 class 𝑏
15	12	cv 1541	. . . . . . . . . 10 class 𝑓
16		vq	. . . . . . . . . . . 12 setvar 𝑞
17	16	cv 1541	. . . . . . . . . . 11 class 𝑞
18	13	cv 1541	. . . . . . . . . . 11 class 𝑔
19		cmulr 17198	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6544	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7409	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18821	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6544	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7409	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 25569	. . . . . . . . . 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 11248	. . . . . . . 8 class <
30	27, 28, 29	wbr 5149	. . . . . . 7 wff (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)
31	30, 16, 14	crio 7364	. . . . . 6 class (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7411	. . . . 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 1542	1 wff quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))))

This definition is referenced by:  q1pval  25671