# Metamath Proof Explorer

## Theorem evlsval

Description: Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses evlsval.q ${⊢}{Q}=\left({I}\mathrm{evalSub}{S}\right)\left({R}\right)$
evlsval.w ${⊢}{W}={I}\mathrm{mPoly}{U}$
evlsval.v ${⊢}{V}={I}\mathrm{mVar}{U}$
evlsval.u ${⊢}{U}={S}{↾}_{𝑠}{R}$
evlsval.t ${⊢}{T}={S}{↑}_{𝑠}\left({{B}}^{{I}}\right)$
evlsval.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
evlsval.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
evlsval.x ${⊢}{X}=\left({x}\in {R}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)$
evlsval.y ${⊢}{Y}=\left({x}\in {I}⟼\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)$
Assertion evlsval ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Q}=\left(\iota {f}\in \left({W}\mathrm{RingHom}{T}\right)|\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 evlsval.q ${⊢}{Q}=\left({I}\mathrm{evalSub}{S}\right)\left({R}\right)$
2 evlsval.w ${⊢}{W}={I}\mathrm{mPoly}{U}$
3 evlsval.v ${⊢}{V}={I}\mathrm{mVar}{U}$
4 evlsval.u ${⊢}{U}={S}{↾}_{𝑠}{R}$
5 evlsval.t ${⊢}{T}={S}{↑}_{𝑠}\left({{B}}^{{I}}\right)$
6 evlsval.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
7 evlsval.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
8 evlsval.x ${⊢}{X}=\left({x}\in {R}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)$
9 evlsval.y ${⊢}{Y}=\left({x}\in {I}⟼\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)$
10 elex ${⊢}{I}\in {Z}\to {I}\in \mathrm{V}$
11 fveq2 ${⊢}{s}={S}\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{S}}$
12 11 adantl ${⊢}\left({i}={I}\wedge {s}={S}\right)\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{S}}$
13 12 csbeq1d
14 fvex ${⊢}{\mathrm{Base}}_{{S}}\in \mathrm{V}$
15 14 a1i ${⊢}\left({i}={I}\wedge {s}={S}\right)\to {\mathrm{Base}}_{{S}}\in \mathrm{V}$
16 simplr ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge {b}={\mathrm{Base}}_{{S}}\right)\to {s}={S}$
17 16 fveq2d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge {b}={\mathrm{Base}}_{{S}}\right)\to \mathrm{SubRing}\left({s}\right)=\mathrm{SubRing}\left({S}\right)$
18 simpll ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge {b}={\mathrm{Base}}_{{S}}\right)\to {i}={I}$
19 oveq1 ${⊢}{s}={S}\to {s}{↾}_{𝑠}{r}={S}{↾}_{𝑠}{r}$
20 19 ad2antlr ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge {b}={\mathrm{Base}}_{{S}}\right)\to {s}{↾}_{𝑠}{r}={S}{↾}_{𝑠}{r}$
21 18 20 oveq12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge {b}={\mathrm{Base}}_{{S}}\right)\to {i}\mathrm{mPoly}\left({s}{↾}_{𝑠}{r}\right)={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)$
22 21 csbeq1d
23 ovexd ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge {b}={\mathrm{Base}}_{{S}}\right)\to {I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\in \mathrm{V}$
24 simprr ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)$
25 simplr ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {s}={S}$
26 simprl ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {b}={\mathrm{Base}}_{{S}}$
27 simpll ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {i}={I}$
28 26 27 oveq12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {{b}}^{{i}}={{\mathrm{Base}}_{{S}}}^{{I}}$
29 25 28 oveq12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {s}{↑}_{𝑠}\left({{b}}^{{i}}\right)={S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)$
30 24 29 oveq12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {w}\mathrm{RingHom}\left({s}{↑}_{𝑠}\left({{b}}^{{i}}\right)\right)=\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)$
31 24 fveq2d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \mathrm{algSc}\left({w}\right)=\mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)$
32 31 coeq2d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {f}\circ \mathrm{algSc}\left({w}\right)={f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)$
33 28 xpeq1d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left({{b}}^{{i}}\right)×\left\{{x}\right\}=\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}$
34 33 mpteq2dv ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left({x}\in {r}⟼\left({{b}}^{{i}}\right)×\left\{{x}\right\}\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)$
35 32 34 eqeq12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left({f}\circ \mathrm{algSc}\left({w}\right)=\left({x}\in {r}⟼\left({{b}}^{{i}}\right)×\left\{{x}\right\}\right)↔{f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\right)$
36 25 oveq1d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {s}{↾}_{𝑠}{r}={S}{↾}_{𝑠}{r}$
37 27 36 oveq12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {i}\mathrm{mVar}\left({s}{↾}_{𝑠}{r}\right)={I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)$
38 37 coeq2d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to {f}\circ \left({i}\mathrm{mVar}\left({s}{↾}_{𝑠}{r}\right)\right)={f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)$
39 28 mpteq1d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left({g}\in \left({{b}}^{{i}}\right)⟼{g}\left({x}\right)\right)=\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)$
40 27 39 mpteq12dv ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left({x}\in {i}⟼\left({g}\in \left({{b}}^{{i}}\right)⟼{g}\left({x}\right)\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)$
41 38 40 eqeq12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left({f}\circ \left({i}\mathrm{mVar}\left({s}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {i}⟼\left({g}\in \left({{b}}^{{i}}\right)⟼{g}\left({x}\right)\right)\right)↔{f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)$
42 35 41 anbi12d ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left(\left({f}\circ \mathrm{algSc}\left({w}\right)=\left({x}\in {r}⟼\left({{b}}^{{i}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({i}\mathrm{mVar}\left({s}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {i}⟼\left({g}\in \left({{b}}^{{i}}\right)⟼{g}\left({x}\right)\right)\right)\right)↔\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
43 30 42 riotaeqbidv ${⊢}\left(\left({i}={I}\wedge {s}={S}\right)\wedge \left({b}={\mathrm{Base}}_{{S}}\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\right)\to \left(\iota {f}\in \left({w}\mathrm{RingHom}\left({s}{↑}_{𝑠}\left({{b}}^{{i}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({w}\right)=\left({x}\in {r}⟼\left({{b}}^{{i}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({i}\mathrm{mVar}\left({s}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {i}⟼\left({g}\in \left({{b}}^{{i}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)=\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
44 43 anassrs ${⊢}\left(\left(\left({i}={I}\wedge {s}={S}\right)\wedge {b}={\mathrm{Base}}_{{S}}\right)\wedge {w}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\to \left(\iota {f}\in \left({w}\mathrm{RingHom}\left({s}{↑}_{𝑠}\left({{b}}^{{i}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({w}\right)=\left({x}\in {r}⟼\left({{b}}^{{i}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({i}\mathrm{mVar}\left({s}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {i}⟼\left({g}\in \left({{b}}^{{i}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)=\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
45 23 44 csbied
46 22 45 eqtrd
47 17 46 mpteq12dv
48 15 47 csbied
49 13 48 eqtrd
50 df-evls
51 fvex ${⊢}\mathrm{SubRing}\left({S}\right)\in \mathrm{V}$
52 51 mptex ${⊢}\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\in \mathrm{V}$
53 49 50 52 ovmpoa ${⊢}\left({I}\in \mathrm{V}\wedge {S}\in \mathrm{CRing}\right)\to {I}\mathrm{evalSub}{S}=\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)$
54 53 fveq1d ${⊢}\left({I}\in \mathrm{V}\wedge {S}\in \mathrm{CRing}\right)\to \left({I}\mathrm{evalSub}{S}\right)\left({R}\right)=\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\left({R}\right)$
55 10 54 sylan ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\right)\to \left({I}\mathrm{evalSub}{S}\right)\left({R}\right)=\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\left({R}\right)$
56 1 55 syl5eq ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\right)\to {Q}=\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\left({R}\right)$
57 56 3adant3 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Q}=\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\left({R}\right)$
58 oveq2 ${⊢}{r}={R}\to {S}{↾}_{𝑠}{r}={S}{↾}_{𝑠}{R}$
59 58 oveq2d ${⊢}{r}={R}\to {I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)$
60 59 oveq1d ${⊢}{r}={R}\to \left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)=\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)$
61 59 fveq2d ${⊢}{r}={R}\to \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)$
62 61 coeq2d ${⊢}{r}={R}\to {f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)={f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)$
63 mpteq1 ${⊢}{r}={R}\to \left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)$
64 62 63 eqeq12d ${⊢}{r}={R}\to \left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)↔{f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\right)$
65 58 oveq2d ${⊢}{r}={R}\to {I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)={I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)$
66 65 coeq2d ${⊢}{r}={R}\to {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)={f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)$
67 66 eqeq1d ${⊢}{r}={R}\to \left({f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)↔{f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)$
68 64 67 anbi12d ${⊢}{r}={R}\to \left(\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)↔\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
69 60 68 riotaeqbidv ${⊢}{r}={R}\to \left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)=\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
70 eqid ${⊢}\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)=\left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)$
71 riotaex ${⊢}\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\in \mathrm{V}$
72 69 70 71 fvmpt ${⊢}{R}\in \mathrm{SubRing}\left({S}\right)\to \left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\left({R}\right)=\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
73 4 oveq2i ${⊢}{I}\mathrm{mPoly}{U}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)$
74 2 73 eqtri ${⊢}{W}={I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)$
75 6 oveq1i ${⊢}{{B}}^{{I}}={{\mathrm{Base}}_{{S}}}^{{I}}$
76 75 oveq2i ${⊢}{S}{↑}_{𝑠}\left({{B}}^{{I}}\right)={S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)$
77 5 76 eqtri ${⊢}{T}={S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)$
78 74 77 oveq12i ${⊢}{W}\mathrm{RingHom}{T}=\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)$
79 78 a1i ${⊢}\top \to {W}\mathrm{RingHom}{T}=\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)$
80 74 fveq2i ${⊢}\mathrm{algSc}\left({W}\right)=\mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)$
81 7 80 eqtri ${⊢}{A}=\mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)$
82 81 coeq2i ${⊢}{f}\circ {A}={f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)$
83 75 xpeq1i ${⊢}\left({{B}}^{{I}}\right)×\left\{{x}\right\}=\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}$
84 83 mpteq2i ${⊢}\left({x}\in {R}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)$
85 8 84 eqtri ${⊢}{X}=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)$
86 82 85 eqeq12i ${⊢}{f}\circ {A}={X}↔{f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)$
87 4 oveq2i ${⊢}{I}\mathrm{mVar}{U}={I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)$
88 3 87 eqtri ${⊢}{V}={I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)$
89 88 coeq2i ${⊢}{f}\circ {V}={f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)$
90 eqid ${⊢}{g}\left({x}\right)={g}\left({x}\right)$
91 75 90 mpteq12i ${⊢}\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right)=\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)$
92 91 mpteq2i ${⊢}\left({x}\in {I}⟼\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)$
93 9 92 eqtri ${⊢}{Y}=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)$
94 89 93 eqeq12i ${⊢}{f}\circ {V}={Y}↔{f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)$
95 86 94 anbi12i ${⊢}\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)↔\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)$
96 95 a1i ${⊢}\top \to \left(\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)↔\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
97 79 96 riotaeqbidv ${⊢}\top \to \left(\iota {f}\in \left({W}\mathrm{RingHom}{T}\right)|\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)\right)=\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
98 97 mptru ${⊢}\left(\iota {f}\in \left({W}\mathrm{RingHom}{T}\right)|\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)\right)=\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {R}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{R}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)$
99 72 98 syl6eqr ${⊢}{R}\in \mathrm{SubRing}\left({S}\right)\to \left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\left({R}\right)=\left(\iota {f}\in \left({W}\mathrm{RingHom}{T}\right)|\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)\right)$
100 99 3ad2ant3 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({r}\in \mathrm{SubRing}\left({S}\right)⟼\left(\iota {f}\in \left(\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)\mathrm{RingHom}\left({S}{↑}_{𝑠}\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)\right)\right)|\left({f}\circ \mathrm{algSc}\left({I}\mathrm{mPoly}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {r}⟼\left({{\mathrm{Base}}_{{S}}}^{{I}}\right)×\left\{{x}\right\}\right)\wedge {f}\circ \left({I}\mathrm{mVar}\left({S}{↾}_{𝑠}{r}\right)\right)=\left({x}\in {I}⟼\left({g}\in \left({{\mathrm{Base}}_{{S}}}^{{I}}\right)⟼{g}\left({x}\right)\right)\right)\right)\right)\right)\left({R}\right)=\left(\iota {f}\in \left({W}\mathrm{RingHom}{T}\right)|\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)\right)$
101 57 100 eqtrd ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Q}=\left(\iota {f}\in \left({W}\mathrm{RingHom}{T}\right)|\left({f}\circ {A}={X}\wedge {f}\circ {V}={Y}\right)\right)$