# Metamath Proof Explorer

## Theorem evls1fval

Description: Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-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}}$
Assertion evls1fval ${⊢}\left({S}\in {V}\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)$

### 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 elex ${⊢}{S}\in {V}\to {S}\in \mathrm{V}$
5 4 adantr ${⊢}\left({S}\in {V}\wedge {R}\in 𝒫{B}\right)\to {S}\in \mathrm{V}$
6 simpr ${⊢}\left({S}\in {V}\wedge {R}\in 𝒫{B}\right)\to {R}\in 𝒫{B}$
7 ovex ${⊢}{{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\in \mathrm{V}$
8 7 mptex ${⊢}\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\in \mathrm{V}$
9 fvex ${⊢}{E}\left({R}\right)\in \mathrm{V}$
10 8 9 coex ${⊢}\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)\in \mathrm{V}$
11 10 a1i ${⊢}\left({S}\in {V}\wedge {R}\in 𝒫{B}\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 {E}\left({R}\right)\in \mathrm{V}$
12 fveq2 ${⊢}{s}={S}\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{S}}$
13 12 adantr ${⊢}\left({s}={S}\wedge {r}={R}\right)\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{S}}$
14 13 3 syl6eqr ${⊢}\left({s}={S}\wedge {r}={R}\right)\to {\mathrm{Base}}_{{s}}={B}$
15 14 csbeq1d
16 3 fvexi ${⊢}{B}\in \mathrm{V}$
17 16 a1i ${⊢}\left({s}={S}\wedge {r}={R}\right)\to {B}\in \mathrm{V}$
18 id ${⊢}{b}={B}\to {b}={B}$
19 oveq1 ${⊢}{b}={B}\to {{b}}^{{1}_{𝑜}}={{B}}^{{1}_{𝑜}}$
20 18 19 oveq12d ${⊢}{b}={B}\to {{b}}^{\left({{b}}^{{1}_{𝑜}}\right)}={{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}$
21 mpteq1 ${⊢}{b}={B}\to \left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)=\left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
22 21 coeq2d ${⊢}{b}={B}\to {x}\circ \left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)={x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
23 20 22 mpteq12dv ${⊢}{b}={B}\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 \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
24 23 coeq1d ${⊢}{b}={B}\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{evalSub}{s}\right)\left({r}\right)=\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{evalSub}{s}\right)\left({r}\right)$
25 24 adantl ${⊢}\left(\left({s}={S}\wedge {r}={R}\right)\wedge {b}={B}\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{evalSub}{s}\right)\left({r}\right)=\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{evalSub}{s}\right)\left({r}\right)$
26 17 25 csbied
27 oveq2 ${⊢}{s}={S}\to {1}_{𝑜}\mathrm{evalSub}{s}={1}_{𝑜}\mathrm{evalSub}{S}$
28 27 2 syl6eqr ${⊢}{s}={S}\to {1}_{𝑜}\mathrm{evalSub}{s}={E}$
29 28 adantr ${⊢}\left({s}={S}\wedge {r}={R}\right)\to {1}_{𝑜}\mathrm{evalSub}{s}={E}$
30 simpr ${⊢}\left({s}={S}\wedge {r}={R}\right)\to {r}={R}$
31 29 30 fveq12d ${⊢}\left({s}={S}\wedge {r}={R}\right)\to \left({1}_{𝑜}\mathrm{evalSub}{s}\right)\left({r}\right)={E}\left({R}\right)$
32 31 coeq2d ${⊢}\left({s}={S}\wedge {r}={R}\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{evalSub}{s}\right)\left({r}\right)=\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)$
33 15 26 32 3eqtrd
34 12 3 syl6eqr ${⊢}{s}={S}\to {\mathrm{Base}}_{{s}}={B}$
35 34 pweqd ${⊢}{s}={S}\to 𝒫{\mathrm{Base}}_{{s}}=𝒫{B}$
36 df-evls1
37 33 35 36 ovmpox ${⊢}\left({S}\in \mathrm{V}\wedge {R}\in 𝒫{B}\wedge \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)\in \mathrm{V}\right)\to {S}{\mathrm{evalSub}}_{1}{R}=\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)$
38 5 6 11 37 syl3anc ${⊢}\left({S}\in {V}\wedge {R}\in 𝒫{B}\right)\to {S}{\mathrm{evalSub}}_{1}{R}=\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)$
39 1 38 syl5eq ${⊢}\left({S}\in {V}\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)$