# Metamath Proof Explorer

## 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 ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 vf ${setvar}{f}$
4 cbs ${class}\mathrm{Base}$
5 cpl1 ${class}{\mathrm{Poly}}_{1}$
6 1 cv ${setvar}{r}$
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 ${setvar}{f}$
10 c0g ${class}{0}_{𝑔}$
11 7 10 cfv ${class}{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}$
12 9 11 wne ${wff}{f}\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)$