Definition df-r1p

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

	Ref	Expression
Assertion	df-r1p	$$⊢{rem}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼⦋{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr1p	$$class{rem}_{\mathrm{1p}}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		cbs	$$class\mathrm{Base}$$
4		cpl1	$$class{\mathrm{Poly}}_1$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
7	6 3	cfv	$$class{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}$$
8		vb	$$setvarb$$
9		vf	$$setvarf$$
10	8	cv	$$setvarb$$
11		vg	$$setvarg$$
12	9	cv	$$setvarf$$
13		csg	$$class{-}_{𝑔}$$
14	6 13	cfv	$$class{-}_{{\mathrm{Poly}}_1\left(r\right)}$$
15		cq1p	$$class{quot}_{\mathrm{1p}}$$
16	5 15	cfv	$$class{quot}_{\mathrm{1p}}\left(r\right)$$
17	11	cv	$$setvarg$$
18	12 17 16	co	$$class\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right)$$
19		cmulr	$$class{\cdot }_{𝑟}$$
20	6 19	cfv	$$class{\cdot }_{{\mathrm{Poly}}_1\left(r\right)}$$
21	18 17 20	co	$$class\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)$$
22	12 21 14	co	$$class\left(f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)$$
23	9 11 10 10 22	cmpo	$$class\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)$$
24	8 7 23	csb	$$class⦋{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)$$
25	1 2 24	cmpt	$$class\left(r\in \mathrm{V}⟼⦋{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)\right)$$
26	0 25	wceq	$$wff{rem}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼⦋{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)\right)$$