Definition df-q1p 26116

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26121. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20328. (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 26111	. 2 class quot1p
2		vr	. . 3 setvar 𝑟
3		cvv 3431	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1546	. . . . 5 class 𝑟
6		cpl1 22162	. . . . 5 class Poly1
7	5, 6	cfv 6485	. . . 4 class (Poly1‘𝑟)
8		vb	. . . . 5 setvar 𝑏
9	4	cv 1546	. . . . . 6 class 𝑝
10		cbs 17170	. . . . . 6 class Base
11	9, 10	cfv 6485	. . . . 5 class (Base‘𝑝)
12		vf	. . . . . 6 setvar 𝑓
13		vg	. . . . . 6 setvar 𝑔
14	8	cv 1546	. . . . . 6 class 𝑏
15	12	cv 1546	. . . . . . . . . 10 class 𝑓
16		vq	. . . . . . . . . . . 12 setvar 𝑞
17	16	cv 1546	. . . . . . . . . . 11 class 𝑞
18	13	cv 1546	. . . . . . . . . . 11 class 𝑔
19		cmulr 17212	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 6485	. . . . . . . . . . 11 class (.r‘𝑝)
21	17, 18, 20	co 7356	. . . . . . . . . 10 class (𝑞(.r‘𝑝)𝑔)
22		csg 18902	. . . . . . . . . . 11 class -g
23	9, 22	cfv 6485	. . . . . . . . . 10 class (-g‘𝑝)
24	15, 21, 23	co 7356	. . . . . . . . 9 class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))
25		cdg1 26037	. . . . . . . . . 10 class deg1
26	5, 25	cfv 6485	. . . . . . . . 9 class (deg1‘𝑟)
27	24, 26	cfv 6485	. . . . . . . 8 class ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)))
28	18, 26	cfv 6485	. . . . . . . 8 class ((deg1‘𝑟)‘𝑔)
29		clt 11170	. . . . . . . 8 class <
30	27, 28, 29	wbr 5072	. . . . . . 7 wff ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)
31	30, 16, 14	crio 7312	. . . . . 6 class (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))
32	12, 13, 14, 14, 31	cmpo 7358	. . . . 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 5153	. 2 class (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))
36	1, 35	wceq 1547	1 wff quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))

This definition is referenced by:  q1pval  26138