Definition df-q1p 25307

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 25312. We actually use the reversed version for better harmony with our divisibility df-dvdsr 19893. (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 25302	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3429	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1538	. . . . 5 class 𝑟
6		cpl1 21358	. . . . 5 class Poly1
7	5, 6	cfv 6426	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1538	. . . . . 6 class 𝑝
10		cbs 16922	. . . . . 6 class Base
11	9, 10	cfv 6426	. . . . 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 16973	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6426	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7267	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18589	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6426	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7267	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 25226	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6426	. . . . . . . . 9 class ( deg1 ‘𝑟)
27	24, 26	cfv 6426	. . . . . . . 8 class (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6426	. . . . . . . 8 class (( deg1 ‘𝑟)‘𝑔)
29		clt 11019	. . . . . . . 8 class <
30	27, 28, 29	wbr 5073	. . . . . . 7 wff (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)
31	30, 16, 14	crio 7223	. . . . . 6 class (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7269	. . . . 5 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
33	8, 11, 32	csb 3831	. . . 4 class ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
34	4, 7, 33	csb 3831	. . 3 class ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))
35	2, 3, 34	cmpt 5156	. 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  25328