Description: Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | deg1xrf.d | |- D = ( deg1 ` R ) |
|
deg1xrf.p | |- P = ( Poly1 ` R ) |
||
deg1xrf.b | |- B = ( Base ` P ) |
||
Assertion | deg1xrf | |- D : B --> RR* |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deg1xrf.d | |- D = ( deg1 ` R ) |
|
2 | deg1xrf.p | |- P = ( Poly1 ` R ) |
|
3 | deg1xrf.b | |- B = ( Base ` P ) |
|
4 | 1 | deg1fval | |- D = ( 1o mDeg R ) |
5 | eqid | |- ( 1o mPoly R ) = ( 1o mPoly R ) |
|
6 | 2 3 | ply1bas | |- B = ( Base ` ( 1o mPoly R ) ) |
7 | 4 5 6 | mdegxrf | |- D : B --> RR* |