# Metamath Proof Explorer

## Theorem evlrhm

Description: The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evlval.q ${⊢}{Q}={I}\mathrm{eval}{R}$
evlval.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
evlrhm.w ${⊢}{W}={I}\mathrm{mPoly}{R}$
evlrhm.t ${⊢}{T}={R}{↑}_{𝑠}\left({{B}}^{{I}}\right)$
Assertion evlrhm ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {Q}\in \left({W}\mathrm{RingHom}{T}\right)$

### Proof

Step Hyp Ref Expression
1 evlval.q ${⊢}{Q}={I}\mathrm{eval}{R}$
2 evlval.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 evlrhm.w ${⊢}{W}={I}\mathrm{mPoly}{R}$
4 evlrhm.t ${⊢}{T}={R}{↑}_{𝑠}\left({{B}}^{{I}}\right)$
5 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
6 5 adantl ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{Ring}$
7 2 subrgid ${⊢}{R}\in \mathrm{Ring}\to {B}\in \mathrm{SubRing}\left({R}\right)$
8 6 7 syl ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {B}\in \mathrm{SubRing}\left({R}\right)$
9 1 2 evlval ${⊢}{Q}=\left({I}\mathrm{evalSub}{R}\right)\left({B}\right)$
10 eqid ${⊢}{I}\mathrm{mPoly}\left({R}{↾}_{𝑠}{B}\right)={I}\mathrm{mPoly}\left({R}{↾}_{𝑠}{B}\right)$
11 eqid ${⊢}{R}{↾}_{𝑠}{B}={R}{↾}_{𝑠}{B}$
12 9 10 11 4 2 evlsrhm ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\wedge {B}\in \mathrm{SubRing}\left({R}\right)\right)\to {Q}\in \left(\left({I}\mathrm{mPoly}\left({R}{↾}_{𝑠}{B}\right)\right)\mathrm{RingHom}{T}\right)$
13 8 12 mpd3an3 ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {Q}\in \left(\left({I}\mathrm{mPoly}\left({R}{↾}_{𝑠}{B}\right)\right)\mathrm{RingHom}{T}\right)$
14 2 ressid ${⊢}{R}\in \mathrm{CRing}\to {R}{↾}_{𝑠}{B}={R}$
15 14 adantl ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {R}{↾}_{𝑠}{B}={R}$
16 15 oveq2d ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {I}\mathrm{mPoly}\left({R}{↾}_{𝑠}{B}\right)={I}\mathrm{mPoly}{R}$
17 16 3 syl6eqr ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {I}\mathrm{mPoly}\left({R}{↾}_{𝑠}{B}\right)={W}$
18 17 oveq1d ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to \left({I}\mathrm{mPoly}\left({R}{↾}_{𝑠}{B}\right)\right)\mathrm{RingHom}{T}={W}\mathrm{RingHom}{T}$
19 13 18 eleqtrd ${⊢}\left({I}\in {V}\wedge {R}\in \mathrm{CRing}\right)\to {Q}\in \left({W}\mathrm{RingHom}{T}\right)$