Definition df-q1p 23892

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

Assertion

Ref	Expression
df-q1p	|- quot1p = ( r e. _V |-> [_ (Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )

Distinct variable group:   f, r, g, b, p, q

Detailed syntax breakdown of Definition df-q1p

Step	Hyp	Ref	Expression
1		cq1p 23887	. 2 class quot1p
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vp	. . . 4 setvar p
5	2	cv 1482	. . . . 5 class r
6		cpl1 19547	. . . . 5 class Poly1
7	5, 6	cfv 5888	. . . 4 class (Poly1 ` r )
8		vb	. . . . 5 setvar b
9	4	cv 1482	. . . . . 6 class p
10		cbs 15857	. . . . . 6 class Base
11	9, 10	cfv 5888	. . . . 5 class ( Base ` p )
12		vf	. . . . . 6 setvar f
13		vg	. . . . . 6 setvar g
14	8	cv 1482	. . . . . 6 class b
15	12	cv 1482	. . . . . . . . . 10 class f
16		vq	. . . . . . . . . . . 12 setvar q
17	16	cv 1482	. . . . . . . . . . 11 class q
18	13	cv 1482	. . . . . . . . . . 11 class g
19		cmulr 15942	. . . . . . . . . . . 12 class .r
20	9, 19	cfv 5888	. . . . . . . . . . 11 class ( .r ` p )
21	17, 18, 20	co 6650	. . . . . . . . . 10 class ( q ( .r ` p ) g )
22		csg 17424	. . . . . . . . . . 11 class -g
23	9, 22	cfv 5888	. . . . . . . . . 10 class ( -g ` p )
24	15, 21, 23	co 6650	. . . . . . . . 9 class ( f ( -g ` p ) ( q ( .r ` p ) g ) )
25		cdg1 23814	. . . . . . . . . 10 class deg1
26	5, 25	cfv 5888	. . . . . . . . 9 class ( deg1 ` r )
27	24, 26	cfv 5888	. . . . . . . 8 class ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) )
28	18, 26	cfv 5888	. . . . . . . 8 class ( ( deg1 ` r ) ` g )
29		clt 10074	. . . . . . . 8 class <
30	27, 28, 29	wbr 4653	. . . . . . 7 wff ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g )
31	30, 16, 14	crio 6610	. . . . . 6 class ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) )
32	12, 13, 14, 14, 31	cmpt2 6652	. . . . 5 class ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) )
33	8, 11, 32	csb 3533	. . . 4 class [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) )
34	4, 7, 33	csb 3533	. . 3 class [_ (Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) )
35	2, 3, 34	cmpt 4729	. 2 class ( r e. _V |-> [_ (Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )
36	1, 35	wceq 1483	1 wff quot1p = ( r e. _V |-> [_ (Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )

This definition is referenced by:  q1pval  23913