This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mplelf.x	$⊢ φ \to X \in B$
Assertion	mplelf	$⊢ φ \to 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 \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		mplelf.x	$⊢ φ \to X \in 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 \subseteq {Base}_{(I mPwSer R)}$
9	8 5	sselid	$⊢ φ \to X \in {Base}_{(I mPwSer R)}$
10	6 2 4 7 9	psrelbas	$⊢ φ \to X : D ⟶ K$