Metamath Proof Explorer


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 )