Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mon1 Structured version   Unicode version

Definition df-mon1 20055
 Description: Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-mon1 Monic1p Poly1 Poly1 coe1 deg1
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-mon1
StepHypRef Expression
1 cmn1 20050 . 2 Monic1p
2 vr . . 3
3 cvv 2958 . . 3
4 vf . . . . . . 7
54cv 1652 . . . . . 6
62cv 1652 . . . . . . . 8
7 cpl1 16573 . . . . . . . 8 Poly1
86, 7cfv 5456 . . . . . . 7 Poly1
9 c0g 13725 . . . . . . 7
108, 9cfv 5456 . . . . . 6 Poly1
115, 10wne 2601 . . . . 5 Poly1
12 cdg1 19979 . . . . . . . . 9 deg1
136, 12cfv 5456 . . . . . . . 8 deg1
145, 13cfv 5456 . . . . . . 7 deg1
15 cco1 16576 . . . . . . . 8 coe1
165, 15cfv 5456 . . . . . . 7 coe1
1714, 16cfv 5456 . . . . . 6 coe1 deg1
18 cur 15664 . . . . . . 7
196, 18cfv 5456 . . . . . 6
2017, 19wceq 1653 . . . . 5 coe1 deg1
2111, 20wa 360 . . . 4 Poly1 coe1 deg1
22 cbs 13471 . . . . 5
238, 22cfv 5456 . . . 4 Poly1
2421, 4, 23crab 2711 . . 3 Poly1 Poly1 coe1 deg1
252, 3, 24cmpt 4268 . 2 Poly1 Poly1 coe1 deg1
261, 25wceq 1653 1 Monic1p Poly1 Poly1 coe1 deg1
 Colors of variables: wff set class This definition is referenced by:  mon1pval  20066
 Copyright terms: Public domain W3C validator