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

Definition df-uc1p 20046
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 20052. (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 20041 . 2  class Unic1p
2 vr . . 3  set  r
3 cvv 2948 . . 3  class  _V
4 vf . . . . . . 7  set  f
54cv 1651 . . . . . 6  class  f
62cv 1651 . . . . . . . 8  class  r
7 cpl1 16563 . . . . . . . 8  class Poly1
86, 7cfv 5446 . . . . . . 7  class  (Poly1 `  r
)
9 c0g 13715 . . . . . . 7  class  0g
108, 9cfv 5446 . . . . . 6  class  ( 0g
`  (Poly1 `  r ) )
115, 10wne 2598 . . . . 5  wff  f  =/=  ( 0g `  (Poly1 `  r ) )
12 cdg1 19969 . . . . . . . . 9  class deg1
136, 12cfv 5446 . . . . . . . 8  class  ( deg1  `  r
)
145, 13cfv 5446 . . . . . . 7  class  ( ( deg1  `  r ) `  f
)
15 cco1 16566 . . . . . . . 8  class coe1
165, 15cfv 5446 . . . . . . 7  class  (coe1 `  f
)
1714, 16cfv 5446 . . . . . 6  class  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )
18 cui 15736 . . . . . . 7  class Unit
196, 18cfv 5446 . . . . . 6  class  (Unit `  r )
2017, 19wcel 1725 . . . . 5  wff  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )  e.  (Unit `  r )
2111, 20wa 359 . . . 4  wff  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f ) `  ( ( deg1  `  r ) `  f ) )  e.  (Unit `  r )
)
22 cbs 13461 . . . . 5  class  Base
238, 22cfv 5446 . . . 4  class  ( Base `  (Poly1 `  r ) )
2421, 4, 23crab 2701 . . 3  class  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) }
252, 3, 24cmpt 4258 . 2  class  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) } )
261, 25wceq 1652 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  20054
  Copyright terms: Public domain W3C validator