Theorem mpff

Description: Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Hypotheses	mpfsubrg.q	$$⊢Q=\mathrm{ran}\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	mpff.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	mpff	$$⊢F\in Q\to F:B^I⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mpfsubrg.q	$$⊢Q=\mathrm{ran}\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		mpff.b	$$⊢B={\mathrm{Base}}_S$$
3	2	eqcomi	$$⊢{\mathrm{Base}}_S=B$$
4	3	oveq1i	$$⊢{{\mathrm{Base}}_S}^I=B^I$$
5	4	oveq2i	$$⊢S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)=S{\uparrow }_{𝑠}\left(B^I\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
7	1	mpfrcl	$$⊢F\in Q\to \left(I\in \mathrm{V}\wedge S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)$$
8	7	simp2d	$$⊢F\in Q\to S\in \mathrm{CRing}$$
9		ovexd	$$⊢F\in Q\to B^I\in \mathrm{V}$$
10	1	mpfsubrg	$$⊢\left(I\in \mathrm{V}\wedge S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to Q\in \mathrm{SubRing}\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)$$
11	6	subrgss	$$⊢Q\in \mathrm{SubRing}\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)\to Q\subseteq {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
12	7 10 11	3syl	$$⊢F\in Q\to Q\subseteq {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
13		id	$$⊢F\in Q\to F\in Q$$
14	12 13	sseldd	$$⊢F\in Q\to F\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left({{\mathrm{Base}}_S}^I\right)\right)}$$
15	5 2 6 8 9 14	pwselbas	$$⊢F\in Q\to F:B^I⟶B$$