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 Poly1 Poly1 coe1 deg1 Unit
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-uc1p
StepHypRef Expression
1 cuc1p 22395 . 2 Unic1p
2 vr . . 3
3 cvv 3118 . . 3
4 vf . . . . . . 7
54cv 1378 . . . . . 6
62cv 1378 . . . . . . . 8
7 cpl1 18086 . . . . . . . 8 Poly1
86, 7cfv 5594 . . . . . . 7 Poly1
9 c0g 14712 . . . . . . 7
108, 9cfv 5594 . . . . . 6 Poly1
115, 10wne 2662 . . . . 5 Poly1
12 cdg1 22320 . . . . . . . . 9 deg1
136, 12cfv 5594 . . . . . . . 8 deg1
145, 13cfv 5594 . . . . . . 7 deg1
15 cco1 18087 . . . . . . . 8 coe1
165, 15cfv 5594 . . . . . . 7 coe1
1714, 16cfv 5594 . . . . . 6 coe1 deg1
18 cui 17160 . . . . . . 7 Unit
196, 18cfv 5594 . . . . . 6 Unit
2017, 19wcel 1767 . . . . 5 coe1 deg1 Unit
2111, 20wa 369 . . . 4 Poly1 coe1 deg1 Unit
22 cbs 14507 . . . . 5
238, 22cfv 5594 . . . 4 Poly1
2421, 4, 23crab 2821 . . 3 Poly1 Poly1 coe1 deg1 Unit
252, 3, 24cmpt 4511 . 2 Poly1 Poly1 coe1 deg1 Unit
261, 25wceq 1379 1 Unic1p Poly1 Poly1 coe1 deg1 Unit
 Colors of variables: wff setvar class This definition is referenced by:  uc1pval  22408
 Copyright terms: Public domain W3C validator