Metamath Proof Explorer


Definition df-uc1p

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 . (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Assertion df-uc1p Unic1p=rVfBasePoly1r|f0Poly1rcoe1fdeg1rfUnitr

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuc1p classUnic1p
1 vr setvarr
2 cvv classV
3 vf setvarf
4 cbs classBase
5 cpl1 classPoly1
6 1 cv setvarr
7 6 5 cfv classPoly1r
8 7 4 cfv classBasePoly1r
9 3 cv setvarf
10 c0g class0𝑔
11 7 10 cfv class0Poly1r
12 9 11 wne wfff0Poly1r
13 cco1 classcoe1
14 9 13 cfv classcoe1f
15 cdg1 classdeg1
16 6 15 cfv classdeg1r
17 9 16 cfv classdeg1rf
18 17 14 cfv classcoe1fdeg1rf
19 cui classUnit
20 6 19 cfv classUnitr
21 18 20 wcel wffcoe1fdeg1rfUnitr
22 12 21 wa wfff0Poly1rcoe1fdeg1rfUnitr
23 22 3 8 crab classfBasePoly1r|f0Poly1rcoe1fdeg1rfUnitr
24 1 2 23 cmpt classrVfBasePoly1r|f0Poly1rcoe1fdeg1rfUnitr
25 0 24 wceq wffUnic1p=rVfBasePoly1r|f0Poly1rcoe1fdeg1rfUnitr