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	sseldi	|- ( ph -> X e. ( Base ` ( I mPwSer R ) ) )
10	6 2 4 7 9	psrelbas	|- ( ph -> X : D --> K )