# Metamath Proof Explorer

## Theorem evl1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015) (Proof shortened by AV, 13-Sep-2019)

Ref Expression
Hypotheses evl1rhm.q ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
evl1rhm.w ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
evl1rhm.t ${⊢}{T}={R}{↑}_{𝑠}{B}$
evl1rhm.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion evl1rhm ${⊢}{R}\in \mathrm{CRing}\to {O}\in \left({P}\mathrm{RingHom}{T}\right)$

### Proof

Step Hyp Ref Expression
1 evl1rhm.q ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
2 evl1rhm.w ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 evl1rhm.t ${⊢}{T}={R}{↑}_{𝑠}{B}$
4 evl1rhm.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
5 eqid ${⊢}{1}_{𝑜}\mathrm{eval}{R}={1}_{𝑜}\mathrm{eval}{R}$
6 1 5 4 evl1fval ${⊢}{O}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \left({1}_{𝑜}\mathrm{eval}{R}\right)$
7 eqid ${⊢}\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
8 4 3 7 evls1rhmlem ${⊢}{R}\in \mathrm{CRing}\to \left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\in \left(\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\mathrm{RingHom}{T}\right)$
9 1on ${⊢}{1}_{𝑜}\in \mathrm{On}$
10 eqid ${⊢}{1}_{𝑜}\mathrm{mPoly}{R}={1}_{𝑜}\mathrm{mPoly}{R}$
11 eqid ${⊢}{R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)={R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)$
12 5 4 10 11 evlrhm ${⊢}\left({1}_{𝑜}\in \mathrm{On}\wedge {R}\in \mathrm{CRing}\right)\to {1}_{𝑜}\mathrm{eval}{R}\in \left(\left({1}_{𝑜}\mathrm{mPoly}{R}\right)\mathrm{RingHom}\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\right)$
13 9 12 mpan ${⊢}{R}\in \mathrm{CRing}\to {1}_{𝑜}\mathrm{eval}{R}\in \left(\left({1}_{𝑜}\mathrm{mPoly}{R}\right)\mathrm{RingHom}\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\right)$
14 eqidd ${⊢}{R}\in \mathrm{CRing}\to {\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
15 eqidd ${⊢}{R}\in \mathrm{CRing}\to {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
16 eqid ${⊢}{\mathrm{PwSer}}_{1}\left({R}\right)={\mathrm{PwSer}}_{1}\left({R}\right)$
17 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
18 2 16 17 ply1bas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
19 18 a1i ${⊢}{R}\in \mathrm{CRing}\to {\mathrm{Base}}_{{P}}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
20 eqid ${⊢}{+}_{{P}}={+}_{{P}}$
21 2 10 20 ply1plusg ${⊢}{+}_{{P}}={+}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
22 21 a1i ${⊢}{R}\in \mathrm{CRing}\to {+}_{{P}}={+}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
23 22 oveqdr ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {x}{+}_{{P}}{y}={x}{+}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}{y}$
24 eqidd ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({x}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}\wedge {y}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}\right)\right)\to {x}{+}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}{y}={x}{+}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}{y}$
25 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
26 2 10 25 ply1mulr ${⊢}{\cdot }_{{P}}={\cdot }_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
27 26 a1i ${⊢}{R}\in \mathrm{CRing}\to {\cdot }_{{P}}={\cdot }_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
28 27 oveqdr ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {x}{\cdot }_{{P}}{y}={x}{\cdot }_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}{y}$
29 eqidd ${⊢}\left({R}\in \mathrm{CRing}\wedge \left({x}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}\wedge {y}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}\right)\right)\to {x}{\cdot }_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}{y}={x}{\cdot }_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}{y}$
30 14 15 19 15 23 24 28 29 rhmpropd ${⊢}{R}\in \mathrm{CRing}\to {P}\mathrm{RingHom}\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)=\left({1}_{𝑜}\mathrm{mPoly}{R}\right)\mathrm{RingHom}\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)$
31 13 30 eleqtrrd ${⊢}{R}\in \mathrm{CRing}\to {1}_{𝑜}\mathrm{eval}{R}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\right)$
32 rhmco ${⊢}\left(\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\in \left(\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\mathrm{RingHom}{T}\right)\wedge {1}_{𝑜}\mathrm{eval}{R}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\right)\right)\to \left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \left({1}_{𝑜}\mathrm{eval}{R}\right)\in \left({P}\mathrm{RingHom}{T}\right)$
33 8 31 32 syl2anc ${⊢}{R}\in \mathrm{CRing}\to \left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \left({1}_{𝑜}\mathrm{eval}{R}\right)\in \left({P}\mathrm{RingHom}{T}\right)$
34 6 33 eqeltrid ${⊢}{R}\in \mathrm{CRing}\to {O}\in \left({P}\mathrm{RingHom}{T}\right)$