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

Definition df-mon1 19516
Description: Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-mon1  |- Monic1p  =  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  =  ( 1r `  r ) ) } )
Distinct variable group:    f, r

Detailed syntax breakdown of Definition df-mon1
StepHypRef Expression
1 cmn1 19511 . 2  class Monic1p
2 vr . . 3  set  r
3 cvv 2788 . . 3  class  _V
4 vf . . . . . . 7  set  f
54cv 1622 . . . . . 6  class  f
62cv 1622 . . . . . . . 8  class  r
7 cpl1 16252 . . . . . . . 8  class Poly1
86, 7cfv 5255 . . . . . . 7  class  (Poly1 `  r
)
9 c0g 13400 . . . . . . 7  class  0g
108, 9cfv 5255 . . . . . 6  class  ( 0g
`  (Poly1 `  r ) )
115, 10wne 2446 . . . . 5  wff  f  =/=  ( 0g `  (Poly1 `  r ) )
12 cdg1 19440 . . . . . . . . 9  class deg1
136, 12cfv 5255 . . . . . . . 8  class  ( deg1  `  r
)
145, 13cfv 5255 . . . . . . 7  class  ( ( deg1  `  r ) `  f
)
15 cco1 16255 . . . . . . . 8  class coe1
165, 15cfv 5255 . . . . . . 7  class  (coe1 `  f
)
1714, 16cfv 5255 . . . . . 6  class  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )
18 cur 15339 . . . . . . 7  class  1r
196, 18cfv 5255 . . . . . 6  class  ( 1r
`  r )
2017, 19wceq 1623 . . . . 5  wff  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )  =  ( 1r `  r
)
2111, 20wa 358 . . . 4  wff  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f ) `  ( ( deg1  `  r ) `  f ) )  =  ( 1r `  r
) )
22 cbs 13148 . . . . 5  class  Base
238, 22cfv 5255 . . . 4  class  ( Base `  (Poly1 `  r ) )
2421, 4, 23crab 2547 . . 3  class  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  =  ( 1r `  r ) ) }
252, 3, 24cmpt 4077 . 2  class  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  =  ( 1r `  r ) ) } )
261, 25wceq 1623 1  wff Monic1p  =  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  =  ( 1r `  r ) ) } )
Colors of variables: wff set class
This definition is referenced by:  mon1pval  19527
  Copyright terms: Public domain W3C validator