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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplelf.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mplelf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mplelf.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mplelf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	mplelf	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		mplelf.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplelf.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		mplelf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mplelf.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5		mplelf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
7		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
8	1 6 3 7	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
9	8 5	sseldi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
10	6 2 4 7 9	psrelbas	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ 𝐾 )