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

Definition df-uc1p 19533
Description: Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 19539. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-uc1p  |- Unic1p  =  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) } )
Distinct variable group:    f, r

Detailed syntax breakdown of Definition df-uc1p
StepHypRef Expression
1 cuc1p 19528 . 2  class Unic1p
2 vr . . 3  set  r
3 cvv 2801 . . 3  class  _V
4 vf . . . . . . 7  set  f
54cv 1631 . . . . . 6  class  f
62cv 1631 . . . . . . . 8  class  r
7 cpl1 16268 . . . . . . . 8  class Poly1
86, 7cfv 5271 . . . . . . 7  class  (Poly1 `  r
)
9 c0g 13416 . . . . . . 7  class  0g
108, 9cfv 5271 . . . . . 6  class  ( 0g
`  (Poly1 `  r ) )
115, 10wne 2459 . . . . 5  wff  f  =/=  ( 0g `  (Poly1 `  r ) )
12 cdg1 19456 . . . . . . . . 9  class deg1
136, 12cfv 5271 . . . . . . . 8  class  ( deg1  `  r
)
145, 13cfv 5271 . . . . . . 7  class  ( ( deg1  `  r ) `  f
)
15 cco1 16271 . . . . . . . 8  class coe1
165, 15cfv 5271 . . . . . . 7  class  (coe1 `  f
)
1714, 16cfv 5271 . . . . . 6  class  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )
18 cui 15437 . . . . . . 7  class Unit
196, 18cfv 5271 . . . . . 6  class  (Unit `  r )
2017, 19wcel 1696 . . . . 5  wff  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )  e.  (Unit `  r )
2111, 20wa 358 . . . 4  wff  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f ) `  ( ( deg1  `  r ) `  f ) )  e.  (Unit `  r )
)
22 cbs 13164 . . . . 5  class  Base
238, 22cfv 5271 . . . 4  class  ( Base `  (Poly1 `  r ) )
2421, 4, 23crab 2560 . . 3  class  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) }
252, 3, 24cmpt 4093 . 2  class  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) } )
261, 25wceq 1632 1  wff Unic1p  =  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) } )
Colors of variables: wff set class
This definition is referenced by:  uc1pval  19541
  Copyright terms: Public domain W3C validator