Description: A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mplelf.p | |- P = ( I mPoly R ) |
|
mplelf.k | |- K = ( Base ` R ) |
||
mplelf.b | |- B = ( Base ` P ) |
||
mplelf.d | |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
||
mplelf.x | |- ( ph -> X e. B ) |
||
Assertion | mplelf | |- ( ph -> X : D --> K ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mplelf.p | |- P = ( I mPoly R ) |
|
2 | mplelf.k | |- K = ( Base ` R ) |
|
3 | mplelf.b | |- B = ( Base ` P ) |
|
4 | mplelf.d | |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
|
5 | mplelf.x | |- ( ph -> X e. B ) |
|
6 | eqid | |- ( I mPwSer R ) = ( I mPwSer R ) |
|
7 | eqid | |- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) ) |
|
8 | 1 6 3 7 | mplbasss | |- B C_ ( Base ` ( I mPwSer R ) ) |
9 | 8 5 | sselid | |- ( ph -> X e. ( Base ` ( I mPwSer R ) ) ) |
10 | 6 2 4 7 9 | psrelbas | |- ( ph -> X : D --> K ) |