Theorem pf1subrg

Description: Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	pf1const.b	$$⊢B={\mathrm{Base}}_R$$
	pf1const.q	$$⊢Q=\mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
Assertion	pf1subrg	$$⊢R\in \mathrm{CRing}\to Q\in \mathrm{SubRing}\left(R{\uparrow }_{𝑠}B\right)$$

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	$$⊢R{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
6	3 4 5 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)$$
7		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
9	7 8	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)}$$
10		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)}$$
11		fnima	$$⊢{\mathrm{eval}}_1\left(R\right)Fn{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\to {\mathrm{eval}}_1\left(R\right)\left[{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right]=\mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
12	6 9 10 11	4syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)\left[{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right]=\mathrm{ran}{\mathrm{eval}}_1\left(R\right)$$
13	12 2	syl6eqr	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)\left[{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right]=Q$$
14	4	ply1assa	$$⊢R\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{AssAlg}$$
15		assaring	$$⊢{\mathrm{Poly}}_1\left(R\right)\in \mathrm{AssAlg}\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{Ring}$$
16	7	subrgid	$$⊢{\mathrm{Poly}}_1\left(R\right)\in \mathrm{Ring}\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
17	14 15 16	3syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
18		rhmima	$$⊢\left({\mathrm{eval}}_1\left(R\right)\in \left({\mathrm{Poly}}_1\left(R\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)\wedge {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(R\right)\right)\right)\to {\mathrm{eval}}_1\left(R\right)\left[{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right]\in \mathrm{SubRing}\left(R{\uparrow }_{𝑠}B\right)$$
19	6 17 18	syl2anc	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)\left[{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right]\in \mathrm{SubRing}\left(R{\uparrow }_{𝑠}B\right)$$
20	13 19	eqeltrrd	$$⊢R\in \mathrm{CRing}\to Q\in \mathrm{SubRing}\left(R{\uparrow }_{𝑠}B\right)$$