Metamath Proof Explorer

Theorem pf1f

Description: Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pf1rcl.q 
|- Q = ran ( eval1 ` R )
pf1f.b 
|- B = ( Base ` R )
Assertion pf1f 
|- ( F e. Q -> F : B --> B )

Proof

Step Hyp Ref Expression
1 pf1rcl.q 
 |-  Q = ran ( eval1 ` R )
2 pf1f.b 
 |-  B = ( Base ` R )
3 eqid 
 |-  ( R ^s B ) = ( R ^s B )
4 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
5 1 pf1rcl 
 |-  ( F e. Q -> R e. CRing )
6 2 fvexi 
 |-  B e. _V
7 6 a1i 
 |-  ( F e. Q -> B e. _V )
8 2 1 pf1subrg 
 |-  ( R e. CRing -> Q e. ( SubRing ` ( R ^s B ) ) )
9 4 subrgss 
 |-  ( Q e. ( SubRing ` ( R ^s B ) ) -> Q C_ ( Base ` ( R ^s B ) ) )
10 5 8 9 3syl 
 |-  ( F e. Q -> Q C_ ( Base ` ( R ^s B ) ) )
11 id 
 |-  ( F e. Q -> F e. Q )
12 10 11 sseldd 
 |-  ( F e. Q -> F e. ( Base ` ( R ^s B ) ) )
13 3 2 4 5 7 12 pwselbas 
 |-  ( F e. Q -> F : B --> B )