Metamath Proof Explorer

Theorem pf1f

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

Ref Expression
Hypotheses pf1rcl.q ${⊢}{Q}=\mathrm{ran}{\mathrm{eval}}_{1}\left({R}\right)$
pf1f.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion pf1f ${⊢}{F}\in {Q}\to {F}:{B}⟶{B}$

Proof

Step Hyp Ref Expression
1 pf1rcl.q ${⊢}{Q}=\mathrm{ran}{\mathrm{eval}}_{1}\left({R}\right)$
2 pf1f.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 eqid ${⊢}{R}{↑}_{𝑠}{B}={R}{↑}_{𝑠}{B}$
4 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
5 1 pf1rcl ${⊢}{F}\in {Q}\to {R}\in \mathrm{CRing}$
6 2 fvexi ${⊢}{B}\in \mathrm{V}$
7 6 a1i ${⊢}{F}\in {Q}\to {B}\in \mathrm{V}$
8 2 1 pf1subrg ${⊢}{R}\in \mathrm{CRing}\to {Q}\in \mathrm{SubRing}\left({R}{↑}_{𝑠}{B}\right)$
9 4 subrgss ${⊢}{Q}\in \mathrm{SubRing}\left({R}{↑}_{𝑠}{B}\right)\to {Q}\subseteq {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
10 5 8 9 3syl ${⊢}{F}\in {Q}\to {Q}\subseteq {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
11 id ${⊢}{F}\in {Q}\to {F}\in {Q}$
12 10 11 sseldd ${⊢}{F}\in {Q}\to {F}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
13 3 2 4 5 7 12 pwselbas ${⊢}{F}\in {Q}\to {F}:{B}⟶{B}$