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{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
4		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}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{\uparrow }_{𝑠}B\right)$$
9	4	subrgss	$$⊢Q\in \mathrm{SubRing}\left(R{\uparrow }_{𝑠}B\right)\to Q\subseteq {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
10	5 8 9	3syl	$$⊢F\in Q\to Q\subseteq {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}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{\uparrow }_{𝑠}B\right)}$$
13	3 2 4 5 7 12	pwselbas	$$⊢F\in Q\to F:B⟶B$$