Definition df-uc1p

Description: Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg . (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	df-uc1p	$$⊢{Unic}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼\left\{f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}|\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuc1p	$$class{Unic}_{\mathrm{1p}}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		cbs	$$class\mathrm{Base}$$
5		cpl1	$$class{\mathrm{Poly}}_1$$
6	1	cv	$$setvarr$$
7	6 5	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
8	7 4	cfv	$$class{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}$$
9	3	cv	$$setvarf$$
10		c0g	$$class{0}_{𝑔}$$
11	7 10	cfv	$$class{0}_{{\mathrm{Poly}}_1\left(r\right)}$$
12	9 11	wne	$$wfff\ne 0_{{\mathrm{Poly}}_1\left(r\right)}$$
13		cco1	$$class{\mathrm{coe}}_1$$
14	9 13	cfv	$$class{\mathrm{coe}}_1\left(f\right)$$
15		cdg1	$$class{\mathrm{deg}}_1$$
16	6 15	cfv	$$class{\mathrm{deg}}_1\left(r\right)$$
17	9 16	cfv	$$class{\mathrm{deg}}_1\left(r\right)\left(f\right)$$
18	17 14	cfv	$$class{\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)$$
19		cui	$$class\mathrm{Unit}$$
20	6 19	cfv	$$class\mathrm{Unit}\left(r\right)$$
21	18 20	wcel	$$wff{\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)$$
22	12 21	wa	$$wff\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\right)$$
23	22 3 8	crab	$$class\left\{f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}|\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\right)\right\}$$
24	1 2 23	cmpt	$$class\left(r\in \mathrm{V}⟼\left\{f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}|\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\right)\right\}\right)$$
25	0 24	wceq	$$wff{Unic}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼\left\{f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}|\left(f\ne 0_{{\mathrm{Poly}}_1\left(r\right)}\wedge {\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)\in \mathrm{Unit}\left(r\right)\right)\right\}\right)$$