Definition df-r1p 25208

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 25203	. 2 class rem1p
2		vr	. . 3 setvar 𝑟
3		cvv 3423	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1538	. . . . . 6 class 𝑟
6		cpl1 21263	. . . . . 6 class Poly1
7	5, 6	cfv 6419	. . . . 5 class (Poly1‘𝑟)
8		cbs 16845	. . . . 5 class Base
9	7, 8	cfv 6419	. . . 4 class (Base‘(Poly1‘𝑟))
10		vf	. . . . 5 setvar 𝑓
11		vg	. . . . 5 setvar 𝑔
12	4	cv 1538	. . . . 5 class 𝑏
13	10	cv 1538	. . . . . 6 class 𝑓
14	11	cv 1538	. . . . . . . 8 class 𝑔
15		cq1p 25202	. . . . . . . . 9 class quot1p
16	5, 15	cfv 6419	. . . . . . . 8 class (quot1p‘𝑟)
17	13, 14, 16	co 7256	. . . . . . 7 class (𝑓(quot1p‘𝑟)𝑔)
18		cmulr 16894	. . . . . . . 8 class .r
19	7, 18	cfv 6419	. . . . . . 7 class (.r‘(Poly1‘𝑟))
20	17, 14, 19	co 7256	. . . . . 6 class ((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)
21		csg 18499	. . . . . . 7 class -g
22	7, 21	cfv 6419	. . . . . 6 class (-g‘(Poly1‘𝑟))
23	13, 20, 22	co 7256	. . . . 5 class (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))
24	10, 11, 12, 12, 23	cmpo 7258	. . . 4 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))
25	4, 9, 24	csb 3829	. . 3 class ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))
26	2, 3, 25	cmpt 5154	. 2 class (𝑟 ∈ V ↦ ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))))
27	1, 26	wceq 1539	1 wff rem1p = (𝑟 ∈ V ↦ ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))))

This definition is referenced by:  r1pval  25231