# Metamath Proof Explorer

## 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}{↑}_{𝑠}{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}{↑}_{𝑠}{B}={R}{↑}_{𝑠}{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}{↑}_{𝑠}{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}{↑}_{𝑠}{B}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
9 7 8 rhmf ${⊢}{\mathrm{eval}}_{1}\left({R}\right)\in \left({\mathrm{Poly}}_{1}\left({R}\right)\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)\to {\mathrm{eval}}_{1}\left({R}\right):{\mathrm{Base}}_{{\mathrm{Poly}}_{1}\left({R}\right)}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
10 ffn ${⊢}{\mathrm{eval}}_{1}\left({R}\right):{\mathrm{Base}}_{{\mathrm{Poly}}_{1}\left({R}\right)}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{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}{↑}_{𝑠}{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}{↑}_{𝑠}{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}{↑}_{𝑠}{B}\right)$
20 13 19 eqeltrrd ${⊢}{R}\in \mathrm{CRing}\to {Q}\in \mathrm{SubRing}\left({R}{↑}_{𝑠}{B}\right)$