Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mnc Unicode version

Definition df-mnc 27440
Description: Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)
Assertion
Ref Expression
df-mnc  |-  Monic  =  ( s  e.  ~P CC  |->  { p  e.  (Poly `  s )  |  ( (coeff `  p ) `  (deg `  p )
)  =  1 } )
Distinct variable group:    s, p

Detailed syntax breakdown of Definition df-mnc
StepHypRef Expression
1 cmnc 27438 . 2  class  Monic
2 vs . . 3  set  s
3 cc 8751 . . . 4  class  CC
43cpw 3638 . . 3  class  ~P CC
5 vp . . . . . . . 8  set  p
65cv 1631 . . . . . . 7  class  p
7 cdgr 19585 . . . . . . 7  class deg
86, 7cfv 5271 . . . . . 6  class  (deg `  p )
9 ccoe 19584 . . . . . . 7  class coeff
106, 9cfv 5271 . . . . . 6  class  (coeff `  p )
118, 10cfv 5271 . . . . 5  class  ( (coeff `  p ) `  (deg `  p ) )
12 c1 8754 . . . . 5  class  1
1311, 12wceq 1632 . . . 4  wff  ( (coeff `  p ) `  (deg `  p ) )  =  1
142cv 1631 . . . . 5  class  s
15 cply 19582 . . . . 5  class Poly
1614, 15cfv 5271 . . . 4  class  (Poly `  s )
1713, 5, 16crab 2560 . . 3  class  { p  e.  (Poly `  s )  |  ( (coeff `  p ) `  (deg `  p ) )  =  1 }
182, 4, 17cmpt 4093 . 2  class  ( s  e.  ~P CC  |->  { p  e.  (Poly `  s )  |  ( (coeff `  p ) `  (deg `  p )
)  =  1 } )
191, 18wceq 1632 1  wff  Monic  =  ( s  e.  ~P CC  |->  { p  e.  (Poly `  s )  |  ( (coeff `  p ) `  (deg `  p )
)  =  1 } )
Colors of variables: wff set class
This definition is referenced by:  elmnc  27444
  Copyright terms: Public domain W3C validator