Definition df-mon1

Description: Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	df-mon1	$$⊢{Monic}_{\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)=1_r\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmn1	$$class{Monic}_{\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		cur	$$class{1}_r$$
20	6 19	cfv	$$class{1}_r$$
21	18 20	wceq	$$wff{\mathrm{coe}}_1\left(f\right)\left({\mathrm{deg}}_1\left(r\right)\left(f\right)\right)=1_r$$
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)=1_r\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)=1_r\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)=1_r\right)\right\}\right)$$
25	0 24	wceq	$$wff{Monic}_{\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)=1_r\right)\right\}\right)$$