# Metamath Proof Explorer

## Theorem evls1val

Description: Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019)

Ref Expression
Hypotheses evls1fval.q ${⊢}{Q}={S}{\mathrm{evalSub}}_{1}{R}$
evls1fval.e ${⊢}{E}={1}_{𝑜}\mathrm{evalSub}{S}$
evls1fval.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
evls1val.m ${⊢}{M}={1}_{𝑜}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)$
evls1val.k ${⊢}{K}={\mathrm{Base}}_{{M}}$
Assertion evls1val ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {Q}\left({A}\right)={E}\left({R}\right)\left({A}\right)\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 evls1fval.q ${⊢}{Q}={S}{\mathrm{evalSub}}_{1}{R}$
2 evls1fval.e ${⊢}{E}={1}_{𝑜}\mathrm{evalSub}{S}$
3 evls1fval.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
4 evls1val.m ${⊢}{M}={1}_{𝑜}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)$
5 evls1val.k ${⊢}{K}={\mathrm{Base}}_{{M}}$
6 3 subrgss ${⊢}{R}\in \mathrm{SubRing}\left({S}\right)\to {R}\subseteq {B}$
7 6 adantl ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {R}\subseteq {B}$
8 elpwg ${⊢}{R}\in \mathrm{SubRing}\left({S}\right)\to \left({R}\in 𝒫{B}↔{R}\subseteq {B}\right)$
9 8 adantl ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({R}\in 𝒫{B}↔{R}\subseteq {B}\right)$
10 7 9 mpbird ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {R}\in 𝒫{B}$
11 1 2 3 evls1fval ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in 𝒫{B}\right)\to {Q}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {E}\left({R}\right)$
12 10 11 syldan ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Q}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {E}\left({R}\right)$
13 12 fveq1d ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Q}\left({A}\right)=\left(\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {E}\left({R}\right)\right)\left({A}\right)$
14 13 3adant3 ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {Q}\left({A}\right)=\left(\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {E}\left({R}\right)\right)\left({A}\right)$
15 1on ${⊢}{1}_{𝑜}\in \mathrm{On}$
16 simp1 ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {S}\in \mathrm{CRing}$
17 simp2 ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {R}\in \mathrm{SubRing}\left({S}\right)$
18 2 fveq1i ${⊢}{E}\left({R}\right)=\left({1}_{𝑜}\mathrm{evalSub}{S}\right)\left({R}\right)$
19 eqid ${⊢}{S}{↾}_{𝑠}{R}={S}{↾}_{𝑠}{R}$
20 eqid ${⊢}{S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)={S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)$
21 18 4 19 20 3 evlsrhm ${⊢}\left({1}_{𝑜}\in \mathrm{On}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {E}\left({R}\right)\in \left({M}\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\right)$
22 15 16 17 21 mp3an2i ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {E}\left({R}\right)\in \left({M}\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\right)$
23 eqid ${⊢}{\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}={\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
24 5 23 rhmf ${⊢}{E}\left({R}\right)\in \left({M}\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)\right)\to {E}\left({R}\right):{K}⟶{\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
25 22 24 syl ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {E}\left({R}\right):{K}⟶{\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
26 simp3 ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {A}\in {K}$
27 fvco3 ${⊢}\left({E}\left({R}\right):{K}⟶{\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}\wedge {A}\in {K}\right)\to \left(\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {E}\left({R}\right)\right)\left({A}\right)=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\left({E}\left({R}\right)\left({A}\right)\right)$
28 25 26 27 syl2anc ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to \left(\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {E}\left({R}\right)\right)\left({A}\right)=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\left({E}\left({R}\right)\left({A}\right)\right)$
29 25 26 ffvelrnd ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {E}\left({R}\right)\left({A}\right)\in {\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
30 ovex ${⊢}{{B}}^{{1}_{𝑜}}\in \mathrm{V}$
31 20 3 pwsbas ${⊢}\left({S}\in \mathrm{CRing}\wedge {{B}}^{{1}_{𝑜}}\in \mathrm{V}\right)\to {{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}={\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
32 16 30 31 sylancl ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}={\mathrm{Base}}_{\left({S}{↑}_{𝑠}\left({{B}}^{{1}_{𝑜}}\right)\right)}$
33 29 32 eleqtrrd ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {E}\left({R}\right)\left({A}\right)\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)$
34 coeq1 ${⊢}{x}={E}\left({R}\right)\left({A}\right)\to {x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)={E}\left({R}\right)\left({A}\right)\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
35 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)$
36 fvex ${⊢}{E}\left({R}\right)\left({A}\right)\in \mathrm{V}$
37 3 fvexi ${⊢}{B}\in \mathrm{V}$
38 37 mptex ${⊢}\left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\in \mathrm{V}$
39 36 38 coex ${⊢}{E}\left({R}\right)\left({A}\right)\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\in \mathrm{V}$
40 34 35 39 fvmpt ${⊢}{E}\left({R}\right)\left({A}\right)\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\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)\left({E}\left({R}\right)\left({A}\right)\right)={E}\left({R}\right)\left({A}\right)\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
41 33 40 syl ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to \left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\left({E}\left({R}\right)\left({A}\right)\right)={E}\left({R}\right)\left({A}\right)\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
42 14 28 41 3eqtrd ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\wedge {A}\in {K}\right)\to {Q}\left({A}\right)={E}\left({R}\right)\left({A}\right)\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$