MPE Home 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  =  ( 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 20050 . 2  class Monic1p
2 vr . . 3  set  r
3 cvv 2958 . . 3  class  _V
4 vf . . . . . . 7  set  f
54cv 1652 . . . . . 6  class  f
62cv 1652 . . . . . . . 8  class  r
7 cpl1 16573 . . . . . . . 8  class Poly1
86, 7cfv 5456 . . . . . . 7  class  (Poly1 `  r
)
9 c0g 13725 . . . . . . 7  class  0g
108, 9cfv 5456 . . . . . 6  class  ( 0g
`  (Poly1 `  r ) )
115, 10wne 2601 . . . . 5  wff  f  =/=  ( 0g `  (Poly1 `  r ) )
12 cdg1 19979 . . . . . . . . 9  class deg1
136, 12cfv 5456 . . . . . . . 8  class  ( deg1  `  r
)
145, 13cfv 5456 . . . . . . 7  class  ( ( deg1  `  r ) `  f
)
15 cco1 16576 . . . . . . . 8  class coe1
165, 15cfv 5456 . . . . . . 7  class  (coe1 `  f
)
1714, 16cfv 5456 . . . . . 6  class  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )
18 cur 15664 . . . . . . 7  class  1r
196, 18cfv 5456 . . . . . 6  class  ( 1r
`  r )
2017, 19wceq 1653 . . . . 5  wff  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )  =  ( 1r `  r
)
2111, 20wa 360 . . . 4  wff  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f ) `  ( ( deg1  `  r ) `  f ) )  =  ( 1r `  r
) )
22 cbs 13471 . . . . 5  class  Base
238, 22cfv 5456 . . . 4  class  ( Base `  (Poly1 `  r ) )
2421, 4, 23crab 2711 . . 3  class  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  =  ( 1r `  r ) ) }
252, 3, 24cmpt 4268 . 2  class  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  =  ( 1r `  r ) ) } )
261, 25wceq 1653 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  20066
  Copyright terms: Public domain W3C validator