Definition df-r1p 23893

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

Assertion

Ref	Expression
df-r1p	|- rem1p = ( r e. _V |-> [_ ( Base ` (Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) ) ) )

Distinct variable group:   f, r, g, b

Detailed syntax breakdown of Definition df-r1p

Step	Hyp	Ref	Expression
1		cr1p 23888	. 2 class rem1p
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . . 6 class r
6		cpl1 19547	. . . . . 6 class Poly1
7	5, 6	cfv 5888	. . . . 5 class (Poly1 ` r )
8		cbs 15857	. . . . 5 class Base
9	7, 8	cfv 5888	. . . 4 class ( Base ` (Poly1 ` r ) )
10		vf	. . . . 5 setvar f
11		vg	. . . . 5 setvar g
12	4	cv 1482	. . . . 5 class b
13	10	cv 1482	. . . . . 6 class f
14	11	cv 1482	. . . . . . . 8 class g
15		cq1p 23887	. . . . . . . . 9 class quot1p
16	5, 15	cfv 5888	. . . . . . . 8 class (quot1p ` r )
17	13, 14, 16	co 6650	. . . . . . 7 class ( f (quot1p ` r ) g )
18		cmulr 15942	. . . . . . . 8 class .r
19	7, 18	cfv 5888	. . . . . . 7 class ( .r ` (Poly1 ` r ) )
20	17, 14, 19	co 6650	. . . . . 6 class ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g )
21		csg 17424	. . . . . . 7 class -g
22	7, 21	cfv 5888	. . . . . 6 class ( -g ` (Poly1 ` r ) )
23	13, 20, 22	co 6650	. . . . 5 class ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) )
24	10, 11, 12, 12, 23	cmpt2 6652	. . . 4 class ( f e. b , g e. b |-> ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) ) )
25	4, 9, 24	csb 3533	. . 3 class [_ ( Base ` (Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) ) )
26	2, 3, 25	cmpt 4729	. 2 class ( r e. _V |-> [_ ( Base ` (Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) ) ) )
27	1, 26	wceq 1483	1 wff rem1p = ( r e. _V |-> [_ ( Base ` (Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` (Poly1 ` r ) ) ( ( f (quot1p ` r ) g ) ( .r ` (Poly1 ` r ) ) g ) ) ) )

This definition is referenced by:  r1pval  23916