Theorem pf1id

Description: The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015)

	Ref	Expression
Hypotheses	pf1const.b	$$⊢B={\mathrm{Base}}_R$$
	pf1const.q	$$⊢Q=\mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
Assertion	pf1id	$$⊢R\in \mathrm{CRing}\to {\mathrm{I}\upharpoonright }_B\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{var}}_1\left(R\right)={\mathrm{var}}_1\left(R\right)$$
5	3 4 1	evl1var	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right)\right)={\mathrm{I}\upharpoonright }_B$$
6		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
7		eqid	$$⊢R{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
8	3 6 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		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
10		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
11	9 10	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)}$$
12		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)}$$
13	8 11 12	3syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)Fn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
14		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
15	4 6 9	vr1cl	$$⊢R\in \mathrm{Ring}\to {\mathrm{var}}_1\left(R\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
16	14 15	syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{var}}_1\left(R\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
17		fnfvelrn	$$⊢\left({\mathrm{eval}}_1\left(R\right)Fn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge {\mathrm{var}}_1\left(R\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right)\right)\in \mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
18	13 16 17	syl2anc	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right)\right)\in \mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
19	5 18	eqeltrrd	$$⊢R\in \mathrm{CRing}\to {\mathrm{I}\upharpoonright }_B\in \mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
20	19 2	eleqtrrdi	$$⊢R\in \mathrm{CRing}\to {\mathrm{I}\upharpoonright }_B\in Q$$