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\mathrm{mPoly}R$$
	mplelf.k	$$⊢K={\mathrm{Base}}_R$$
	mplelf.b	$$⊢B={\mathrm{Base}}_P$$
	mplelf.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplelf.x	$$⊢\phi \to X\in B$$
Assertion	mplelf	$$⊢\phi \to X:D⟶K$$

Proof

Step	Hyp	Ref	Expression
1		mplelf.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplelf.k	$$⊢K={\mathrm{Base}}_R$$
3		mplelf.b	$$⊢B={\mathrm{Base}}_P$$
4		mplelf.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		mplelf.x	$$⊢\phi \to X\in B$$
6		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
8	1 6 3 7	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
9	8 5	sseldi	$$⊢\phi \to X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
10	6 2 4 7 9	psrelbas	$$⊢\phi \to X:D⟶K$$