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

Definition df-mon1 22404
 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 22399 . 2 Monic1p
2 vr . . 3
3 cvv 3095 . . 3
4 vf . . . . . . 7
54cv 1382 . . . . . 6
62cv 1382 . . . . . . . 8
7 cpl1 18090 . . . . . . . 8 Poly1
86, 7cfv 5578 . . . . . . 7 Poly1
9 c0g 14714 . . . . . . 7
108, 9cfv 5578 . . . . . 6 Poly1
115, 10wne 2638 . . . . 5 Poly1
12 cdg1 22325 . . . . . . . . 9 deg1
136, 12cfv 5578 . . . . . . . 8 deg1
145, 13cfv 5578 . . . . . . 7 deg1
15 cco1 18091 . . . . . . . 8 coe1
165, 15cfv 5578 . . . . . . 7 coe1
1714, 16cfv 5578 . . . . . 6 coe1 deg1
18 cur 17027 . . . . . . 7
196, 18cfv 5578 . . . . . 6
2017, 19wceq 1383 . . . . 5 coe1 deg1
2111, 20wa 369 . . . 4 Poly1 coe1 deg1
22 cbs 14509 . . . . 5
238, 22cfv 5578 . . . 4 Poly1
2421, 4, 23crab 2797 . . 3 Poly1 Poly1 coe1 deg1
252, 3, 24cmpt 4495 . 2 Poly1 Poly1 coe1 deg1
261, 25wceq 1383 1 Monic1p Poly1 Poly1 coe1 deg1
 Colors of variables: wff setvar class This definition is referenced by:  mon1pval  22415
 Copyright terms: Public domain W3C validator