# Metamath Proof Explorer

## Theorem evl1fval

Description: Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1fval.o ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
evl1fval.q ${⊢}{Q}={1}_{𝑜}\mathrm{eval}{R}$
evl1fval.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion 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 {Q}$

### Proof

Step Hyp Ref Expression
1 evl1fval.o ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
2 evl1fval.q ${⊢}{Q}={1}_{𝑜}\mathrm{eval}{R}$
3 evl1fval.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
4 fvexd ${⊢}{r}={R}\to {\mathrm{Base}}_{{r}}\in \mathrm{V}$
5 id ${⊢}{b}={\mathrm{Base}}_{{r}}\to {b}={\mathrm{Base}}_{{r}}$
6 fveq2 ${⊢}{r}={R}\to {\mathrm{Base}}_{{r}}={\mathrm{Base}}_{{R}}$
7 6 3 syl6eqr ${⊢}{r}={R}\to {\mathrm{Base}}_{{r}}={B}$
8 5 7 sylan9eqr ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to {b}={B}$
9 8 oveq1d ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to {{b}}^{{1}_{𝑜}}={{B}}^{{1}_{𝑜}}$
10 8 9 oveq12d ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to {{b}}^{\left({{b}}^{{1}_{𝑜}}\right)}={{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}$
11 8 mpteq1d ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to \left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)=\left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
12 11 coeq2d ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to {x}\circ \left({y}\in {b}⟼{1}_{𝑜}×\left\{{y}\right\}\right)={x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)$
13 10 12 mpteq12dv ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{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)=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)$
14 simpl ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to {r}={R}$
15 14 oveq2d ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to {1}_{𝑜}\mathrm{eval}{r}={1}_{𝑜}\mathrm{eval}{R}$
16 15 2 syl6eqr ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{r}}\right)\to {1}_{𝑜}\mathrm{eval}{r}={Q}$
17 13 16 coeq12d ${⊢}\left({r}={R}\wedge {b}={\mathrm{Base}}_{{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{eval}{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 {Q}$
18 4 17 csbied
19 df-evl1
20 ovex ${⊢}{{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\in \mathrm{V}$
21 20 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}$
22 2 ovexi ${⊢}{Q}\in \mathrm{V}$
23 21 22 coex ${⊢}\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {Q}\in \mathrm{V}$
24 18 19 23 fvmpt ${⊢}{R}\in \mathrm{V}\to {\mathrm{eval}}_{1}\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 {Q}$
25 1 24 syl5eq ${⊢}{R}\in \mathrm{V}\to {O}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {Q}$
26 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{eval}}_{1}\left({R}\right)=\varnothing$
27 1 26 syl5eq ${⊢}¬{R}\in \mathrm{V}\to {O}=\varnothing$
28 co02 ${⊢}\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \varnothing =\varnothing$
29 27 28 syl6eqr ${⊢}¬{R}\in \mathrm{V}\to {O}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \varnothing$
30 df-evl ${⊢}\mathrm{eval}=\left({i}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({i}\mathrm{evalSub}{r}\right)\left({\mathrm{Base}}_{{r}}\right)\right)$
31 30 reldmmpo ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{eval}$
32 31 ovprc2 ${⊢}¬{R}\in \mathrm{V}\to {1}_{𝑜}\mathrm{eval}{R}=\varnothing$
33 2 32 syl5eq ${⊢}¬{R}\in \mathrm{V}\to {Q}=\varnothing$
34 33 coeq2d ${⊢}¬{R}\in \mathrm{V}\to \left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {Q}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \varnothing$
35 29 34 eqtr4d ${⊢}¬{R}\in \mathrm{V}\to {O}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {Q}$
36 25 35 pm2.61i ${⊢}{O}=\left({x}\in \left({{B}}^{\left({{B}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {B}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ {Q}$