Theorem mpff

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

	Ref	Expression
Hypotheses	mpfsubrg.q	|- Q = ran ( ( I evalSub S ) ` R )
	mpff.b	|- B = ( Base ` S )
Assertion	mpff	|- ( F e. Q -> F : ( B ^m I ) --> B )

Proof

Step	Hyp	Ref	Expression
1		mpfsubrg.q	|- Q = ran ( ( I evalSub S ) ` R )
2		mpff.b	|- B = ( Base ` S )
3	2	eqcomi	|- ( Base ` S ) = B
4	3	oveq1i	|- ( ( Base ` S ) ^m I ) = ( B ^m I )
5	4	oveq2i	|- ( S ^s ( ( Base ` S ) ^m I ) ) = ( S ^s ( B ^m I ) )
6		eqid	|- ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) )
7	1	mpfrcl	|- ( F e. Q -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) )
8	7	simp2d	|- ( F e. Q -> S e. CRing )
9		ovexd	|- ( F e. Q -> ( B ^m I ) e. _V )
10	1	mpfsubrg	|- ( ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
11	6	subrgss	|- ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
12	7 10 11	3syl	|- ( F e. Q -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
13		id	|- ( F e. Q -> F e. Q )
14	12 13	sseldd	|- ( F e. Q -> F e. ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
15	5 2 6 8 9 14	pwselbas	|- ( F e. Q -> F : ( B ^m I ) --> B )