Metamath Proof Explorer


Definition df-mnc

Description: Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014)

Ref Expression
Assertion df-mnc Monic = s 𝒫 p Poly s | coeff p deg p = 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmnc class Monic
1 vs setvar s
2 cc class
3 2 cpw class 𝒫
4 vp setvar p
5 cply class Poly
6 1 cv setvar s
7 6 5 cfv class Poly s
8 ccoe class coeff
9 4 cv setvar p
10 9 8 cfv class coeff p
11 cdgr class deg
12 9 11 cfv class deg p
13 12 10 cfv class coeff p deg p
14 c1 class 1
15 13 14 wceq wff coeff p deg p = 1
16 15 4 7 crab class p Poly s | coeff p deg p = 1
17 1 3 16 cmpt class s 𝒫 p Poly s | coeff p deg p = 1
18 0 17 wceq wff Monic = s 𝒫 p Poly s | coeff p deg p = 1