Definition df-q1p 25306

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 25311. We actually use the reversed version for better harmony with our divisibility df-dvdsr 19892. (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 25301	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3433	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1538	. . . . 5 class 𝑟
6		cpl1 21357	. . . . 5 class Poly1
7	5, 6	cfv 6437	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1538	. . . . . 6 class 𝑝
10		cbs 16921	. . . . . 6 class Base
11	9, 10	cfv 6437	. . . . 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 16972	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6437	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7284	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18588	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6437	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7284	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 25225	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6437	. . . . . . . . 9 class ( deg1 ‘𝑟)
27	24, 26	cfv 6437	. . . . . . . 8 class (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6437	. . . . . . . 8 class (( deg1 ‘𝑟)‘𝑔)
29		clt 11018	. . . . . . . 8 class <
30	27, 28, 29	wbr 5075	. . . . . . 7 wff (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)
31	30, 16, 14	crio 7240	. . . . . 6 class (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7286	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3833	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3833	. . 3 class ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
35	2, 3, 34	cmpt 5158	. 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  25327