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

Definition df-uc1p 22400
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 22406. (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 22395 . 2  class Unic1p
2 vr . . 3  setvar  r
3 cvv 3118 . . 3  class  _V
4 vf . . . . . . 7  setvar  f
54cv 1378 . . . . . 6  class  f
62cv 1378 . . . . . . . 8  class  r
7 cpl1 18086 . . . . . . . 8  class Poly1
86, 7cfv 5594 . . . . . . 7  class  (Poly1 `  r
)
9 c0g 14712 . . . . . . 7  class  0g
108, 9cfv 5594 . . . . . 6  class  ( 0g
`  (Poly1 `  r ) )
115, 10wne 2662 . . . . 5  wff  f  =/=  ( 0g `  (Poly1 `  r ) )
12 cdg1 22320 . . . . . . . . 9  class deg1
136, 12cfv 5594 . . . . . . . 8  class  ( deg1  `  r
)
145, 13cfv 5594 . . . . . . 7  class  ( ( deg1  `  r ) `  f
)
15 cco1 18087 . . . . . . . 8  class coe1
165, 15cfv 5594 . . . . . . 7  class  (coe1 `  f
)
1714, 16cfv 5594 . . . . . 6  class  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )
18 cui 17160 . . . . . . 7  class Unit
196, 18cfv 5594 . . . . . 6  class  (Unit `  r )
2017, 19wcel 1767 . . . . 5  wff  ( (coe1 `  f ) `  (
( deg1  `
 r ) `  f ) )  e.  (Unit `  r )
2111, 20wa 369 . . . 4  wff  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f ) `  ( ( deg1  `  r ) `  f ) )  e.  (Unit `  r )
)
22 cbs 14507 . . . . 5  class  Base
238, 22cfv 5594 . . . 4  class  ( Base `  (Poly1 `  r ) )
2421, 4, 23crab 2821 . . 3  class  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) }
252, 3, 24cmpt 4511 . 2  class  ( r  e.  _V  |->  { f  e.  ( Base `  (Poly1 `  r ) )  |  ( f  =/=  ( 0g `  (Poly1 `  r ) )  /\  ( (coe1 `  f
) `  ( ( deg1  `  r ) `  f
) )  e.  (Unit `  r ) ) } )
261, 25wceq 1379 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 setvar class
This definition is referenced by:  uc1pval  22408
  Copyright terms: Public domain W3C validator