# Metamath Proof Explorer

## Theorem evls1rhmlem

Description: Lemma for evl1rhm and evls1rhm (formerly part of the proof of evl1rhm ): The first function of the composition forming the univariate polynomial evaluation map function for a (sub)ring is a ring homomorphism. (Contributed by AV, 11-Sep-2019)

Ref Expression
Hypotheses evl1rhmlem.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
evl1rhmlem.t ${⊢}{T}={R}{↑}_{𝑠}{B}$
evl1rhmlem.f ${⊢}{F}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
Assertion evls1rhmlem ${⊢}{R}\in \mathrm{CRing}\to {F}\in \left(\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\mathrm{RingHom}{T}\right)$

### Proof

Step Hyp Ref Expression
1 evl1rhmlem.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 evl1rhmlem.t ${⊢}{T}={R}{↑}_{𝑠}{B}$
3 evl1rhmlem.f ${⊢}{F}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
4 ovex ${⊢}{{B}}^{{1}_{𝑜}}\in \mathrm{V}$
5 eqid ${⊢}{R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)={R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)$
6 5 1 pwsbas ${⊢}\left({R}\in \mathrm{CRing}\wedge {{B}}^{{1}_{𝑜}}\in \mathrm{V}\right)\to {{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
7 4 6 mpan2 ${⊢}{R}\in \mathrm{CRing}\to {{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
8 7 mpteq1d ${⊢}{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)=\left({x}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
9 3 8 syl5eq ${⊢}{R}\in \mathrm{CRing}\to {F}=\left({x}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
10 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
11 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
12 1 fvexi ${⊢}{B}\in \mathrm{V}$
13 12 a1i ${⊢}{R}\in \mathrm{CRing}\to {B}\in \mathrm{V}$
14 4 a1i ${⊢}{R}\in \mathrm{CRing}\to {{B}}^{{1}_{𝑜}}\in \mathrm{V}$
15 df1o2 ${⊢}{1}_{𝑜}=\left\{\varnothing \right\}$
16 0ex ${⊢}\varnothing \in \mathrm{V}$
17 eqid ${⊢}\left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)=\left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
18 15 12 16 17 mapsnf1o3 ${⊢}\left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right):{B}\underset{1-1 onto}{⟶}{{B}}^{{1}_{𝑜}}$
19 f1of ${⊢}\left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right):{B}\underset{1-1 onto}{⟶}{{B}}^{{1}_{𝑜}}\to \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right):{B}⟶{{B}}^{{1}_{𝑜}}$
20 18 19 mp1i ${⊢}{R}\in \mathrm{CRing}\to \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right):{B}⟶{{B}}^{{1}_{𝑜}}$
21 2 5 10 11 13 14 20 pwsco1rhm ${⊢}{R}\in \mathrm{CRing}\to \left({x}\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}\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)$
22 9 21 eqeltrd ${⊢}{R}\in \mathrm{CRing}\to {F}\in \left(\left({R}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\mathrm{RingHom}{T}\right)$