Definition df-r1p 25305

Description: Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)

Assertion

Ref	Expression
df-r1p	⊢ rem1p = (𝑟 ∈ V ↦ ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))))

Distinct variable group:   𝑓,𝑟,𝑔,𝑏

Detailed syntax breakdown of Definition df-r1p

Step	Hyp	Ref	Expression
1		cr1p 25300	. 2 class rem1p
2		vr	. . 3 setvar 𝑟
3		cvv 3431	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1537	. . . . . 6 class 𝑟
6		cpl1 21355	. . . . . 6 class Poly1
7	5, 6	cfv 6435	. . . . 5 class (Poly1‘𝑟)
8		cbs 16919	. . . . 5 class Base
9	7, 8	cfv 6435	. . . 4 class (Base‘(Poly1‘𝑟))
10		vf	. . . . 5 setvar 𝑓
11		vg	. . . . 5 setvar 𝑔
12	4	cv 1537	. . . . 5 class 𝑏
13	10	cv 1537	. . . . . 6 class 𝑓
14	11	cv 1537	. . . . . . . 8 class 𝑔
15		cq1p 25299	. . . . . . . . 9 class quot1p
16	5, 15	cfv 6435	. . . . . . . 8 class (quot1p‘𝑟)
17	13, 14, 16	co 7282	. . . . . . 7 class (𝑓(quot1p‘𝑟)𝑔)
18		cmulr 16970	. . . . . . . 8 class .r
19	7, 18	cfv 6435	. . . . . . 7 class (.r‘(Poly1‘𝑟))
20	17, 14, 19	co 7282	. . . . . 6 class ((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)
21		csg 18586	. . . . . . 7 class -g
22	7, 21	cfv 6435	. . . . . 6 class (-g‘(Poly1‘𝑟))
23	13, 20, 22	co 7282	. . . . 5 class (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))
24	10, 11, 12, 12, 23	cmpo 7284	. . . 4 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))
25	4, 9, 24	csb 3831	. . 3 class ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))
26	2, 3, 25	cmpt 5156	. 2 class (𝑟 ∈ V ↦ ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))))
27	1, 26	wceq 1538	1 wff rem1p = (𝑟 ∈ V ↦ ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))))

This definition is referenced by:  r1pval  25328