Theorem pf1const

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

	Ref	Expression
Hypotheses	pf1const.b	$$⊢B={\mathrm{Base}}_R$$
	pf1const.q	$$⊢Q=\mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
Assertion	pf1const	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to B\times \left\{X\right\}\in Q$$

Proof

Step	Hyp	Ref	Expression
1		pf1const.b	$$⊢B={\mathrm{Base}}_R$$
2		pf1const.q	$$⊢Q=\mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
3		eqid	$$⊢{\mathrm{eval}}_1\left(R\right)={\mathrm{eval}}_1\left(R\right)$$
4		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
5		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
6	3 4 1 5	evl1sca	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to {\mathrm{eval}}_1\left(R\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(X\right)\right)=B\times \left\{X\right\}$$
7		eqid	$$⊢R{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
8	3 4 7 1	evl1rhm	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)\in \left({\mathrm{Poly}}_1\left(R\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)$$
9	8	adantr	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to {\mathrm{eval}}_1\left(R\right)\in \left({\mathrm{Poly}}_1\left(R\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
11		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
12	10 11	rhmf	$$⊢{\mathrm{eval}}_1\left(R\right)\in \left({\mathrm{Poly}}_1\left(R\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)\to {\mathrm{eval}}_1\left(R\right):{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
13		ffn	$$⊢{\mathrm{eval}}_1\left(R\right):{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}\to {\mathrm{eval}}_1\left(R\right)Fn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
14	9 12 13	3syl	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to {\mathrm{eval}}_1\left(R\right)Fn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
15		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
16	15	adantr	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to R\in \mathrm{Ring}$$
17	4 5 1 10	ply1sclf	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right):B⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
18	16 17	syl	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right):B⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
19		ffvelrn	$$⊢\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right):B⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge X\in B\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(X\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
20	18 19	sylancom	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(X\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
21		fnfvelrn	$$⊢\left({\mathrm{eval}}_1\left(R\right)Fn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(X\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to {\mathrm{eval}}_1\left(R\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(X\right)\right)\in \mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
22	14 20 21	syl2anc	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to {\mathrm{eval}}_1\left(R\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(X\right)\right)\in \mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
23	6 22	eqeltrrd	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to B\times \left\{X\right\}\in \mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
24	23 2	eleqtrrdi	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to B\times \left\{X\right\}\in Q$$