Definition df-q1p

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg . We actually use the reversed version for better harmony with our divisibility df-dvdsr . (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	df-q1p	$$⊢{quot}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼⦋{\mathrm{Poly}}_1\left(r\right)/p⦌⦋{\mathrm{Base}}_p/b⦌\left(f\in b,g\in b⟼\left(\iota q\in b|{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cq1p	$$class{quot}_{\mathrm{1p}}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		cpl1	$$class{\mathrm{Poly}}_1$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
6		vp	$$setvarp$$
7		cbs	$$class\mathrm{Base}$$
8	6	cv	$$setvarp$$
9	8 7	cfv	$$class{\mathrm{Base}}_p$$
10		vb	$$setvarb$$
11		vf	$$setvarf$$
12	10	cv	$$setvarb$$
13		vg	$$setvarg$$
14		vq	$$setvarq$$
15		cdg1	$$class{\mathrm{deg}}_1$$
16	4 15	cfv	$$class{\mathrm{deg}}_1\left(r\right)$$
17	11	cv	$$setvarf$$
18		csg	$$class{-}_{𝑔}$$
19	8 18	cfv	$$class{-}_p$$
20	14	cv	$$setvarq$$
21		cmulr	$$class{\cdot }_{𝑟}$$
22	8 21	cfv	$$class{\cdot }_p$$
23	13	cv	$$setvarg$$
24	20 23 22	co	$$class\left(q{\cdot }_{p}g\right)$$
25	17 24 19	co	$$class\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)$$
26	25 16	cfv	$$class{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)$$
27		clt	$$class<$$
28	23 16	cfv	$$class{\mathrm{deg}}_1\left(r\right)\left(g\right)$$
29	26 28 27	wbr	$$wff{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)$$
30	29 14 12	crio	$$class\left(\iota q\in b|{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)\right)$$
31	11 13 12 12 30	cmpo	$$class\left(f\in b,g\in b⟼\left(\iota q\in b|{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)\right)\right)$$
32	10 9 31	csb	$$class⦋{\mathrm{Base}}_p/b⦌\left(f\in b,g\in b⟼\left(\iota q\in b|{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)\right)\right)$$
33	6 5 32	csb	$$class⦋{\mathrm{Poly}}_1\left(r\right)/p⦌⦋{\mathrm{Base}}_p/b⦌\left(f\in b,g\in b⟼\left(\iota q\in b|{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)\right)\right)$$
34	1 2 33	cmpt	$$class\left(r\in \mathrm{V}⟼⦋{\mathrm{Poly}}_1\left(r\right)/p⦌⦋{\mathrm{Base}}_p/b⦌\left(f\in b,g\in b⟼\left(\iota q\in b|{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)\right)\right)\right)$$
35	0 34	wceq	$$wff{quot}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼⦋{\mathrm{Poly}}_1\left(r\right)/p⦌⦋{\mathrm{Base}}_p/b⦌\left(f\in b,g\in b⟼\left(\iota q\in b|{\mathrm{deg}}_1\left(r\right)\left(f{-}_p\left(q{\cdot }_{p}g\right)\right)<{\mathrm{deg}}_1\left(r\right)\left(g\right)\right)\right)\right)$$