Metamath Proof Explorer


Theorem mplelf

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 )

Proof

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 )