# Metamath Proof Explorer

## Theorem evlsval2

Description: Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-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 evlsval2 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({Q}\in \left({W}\mathrm{RingHom}{T}\right)\wedge \left({Q}\circ {A}={X}\wedge {Q}\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 1 2 3 4 5 6 7 8 9 evlsval ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Q}=\left(\iota {m}\in \left({W}\mathrm{RingHom}{T}\right)|\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\right)$
11 eqid ${⊢}{\mathrm{Base}}_{{T}}={\mathrm{Base}}_{{T}}$
12 elex ${⊢}{I}\in {Z}\to {I}\in \mathrm{V}$
13 12 3ad2ant1 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {I}\in \mathrm{V}$
14 4 subrgcrng ${⊢}\left({S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {U}\in \mathrm{CRing}$
15 14 3adant1 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {U}\in \mathrm{CRing}$
16 simp2 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {S}\in \mathrm{CRing}$
17 ovex ${⊢}{{B}}^{{I}}\in \mathrm{V}$
18 5 pwscrng ${⊢}\left({S}\in \mathrm{CRing}\wedge {{B}}^{{I}}\in \mathrm{V}\right)\to {T}\in \mathrm{CRing}$
19 16 17 18 sylancl ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {T}\in \mathrm{CRing}$
20 6 subrgss ${⊢}{R}\in \mathrm{SubRing}\left({S}\right)\to {R}\subseteq {B}$
21 20 3ad2ant3 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {R}\subseteq {B}$
22 21 resmptd ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {\left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)↾}_{{R}}=\left({x}\in {R}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)$
23 22 8 syl6eqr ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {\left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)↾}_{{R}}={X}$
24 crngring ${⊢}{S}\in \mathrm{CRing}\to {S}\in \mathrm{Ring}$
25 24 3ad2ant2 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {S}\in \mathrm{Ring}$
26 eqid ${⊢}\left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)=\left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)$
27 5 6 26 pwsdiagrhm ${⊢}\left({S}\in \mathrm{Ring}\wedge {{B}}^{{I}}\in \mathrm{V}\right)\to \left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)\in \left({S}\mathrm{RingHom}{T}\right)$
28 25 17 27 sylancl ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)\in \left({S}\mathrm{RingHom}{T}\right)$
29 simp3 ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {R}\in \mathrm{SubRing}\left({S}\right)$
30 4 resrhm ${⊢}\left(\left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)\in \left({S}\mathrm{RingHom}{T}\right)\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {\left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)↾}_{{R}}\in \left({U}\mathrm{RingHom}{T}\right)$
31 28 29 30 syl2anc ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {\left({x}\in {B}⟼\left({{B}}^{{I}}\right)×\left\{{x}\right\}\right)↾}_{{R}}\in \left({U}\mathrm{RingHom}{T}\right)$
32 23 31 eqeltrrd ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {X}\in \left({U}\mathrm{RingHom}{T}\right)$
33 6 fvexi ${⊢}{B}\in \mathrm{V}$
34 simpl1 ${⊢}\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\to {I}\in {Z}$
35 elmapg ${⊢}\left({B}\in \mathrm{V}\wedge {I}\in {Z}\right)\to \left({g}\in \left({{B}}^{{I}}\right)↔{g}:{I}⟶{B}\right)$
36 33 34 35 sylancr ${⊢}\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\to \left({g}\in \left({{B}}^{{I}}\right)↔{g}:{I}⟶{B}\right)$
37 36 biimpa ${⊢}\left(\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\wedge {g}\in \left({{B}}^{{I}}\right)\right)\to {g}:{I}⟶{B}$
38 simplr ${⊢}\left(\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\wedge {g}\in \left({{B}}^{{I}}\right)\right)\to {x}\in {I}$
39 37 38 ffvelrnd ${⊢}\left(\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\wedge {g}\in \left({{B}}^{{I}}\right)\right)\to {g}\left({x}\right)\in {B}$
40 39 fmpttd ${⊢}\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\to \left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right):{{B}}^{{I}}⟶{B}$
41 simpl2 ${⊢}\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\to {S}\in \mathrm{CRing}$
42 5 6 11 pwselbasb ${⊢}\left({S}\in \mathrm{CRing}\wedge {{B}}^{{I}}\in \mathrm{V}\right)\to \left(\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right)\in {\mathrm{Base}}_{{T}}↔\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right):{{B}}^{{I}}⟶{B}\right)$
43 41 17 42 sylancl ${⊢}\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\to \left(\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right)\in {\mathrm{Base}}_{{T}}↔\left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right):{{B}}^{{I}}⟶{B}\right)$
44 40 43 mpbird ${⊢}\left(\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\wedge {x}\in {I}\right)\to \left({g}\in \left({{B}}^{{I}}\right)⟼{g}\left({x}\right)\right)\in {\mathrm{Base}}_{{T}}$
45 44 9 fmptd ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Y}:{I}⟶{\mathrm{Base}}_{{T}}$
46 2 11 7 3 13 15 19 32 45 evlseu ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to \exists !{m}\in \left({W}\mathrm{RingHom}{T}\right)\phantom{\rule{.4em}{0ex}}\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)$
47 riotacl2 ${⊢}\exists !{m}\in \left({W}\mathrm{RingHom}{T}\right)\phantom{\rule{.4em}{0ex}}\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\to \left(\iota {m}\in \left({W}\mathrm{RingHom}{T}\right)|\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\right)\in \left\{{m}\in \left({W}\mathrm{RingHom}{T}\right)|\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\right\}$
48 46 47 syl ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to \left(\iota {m}\in \left({W}\mathrm{RingHom}{T}\right)|\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\right)\in \left\{{m}\in \left({W}\mathrm{RingHom}{T}\right)|\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\right\}$
49 10 48 eqeltrd ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to {Q}\in \left\{{m}\in \left({W}\mathrm{RingHom}{T}\right)|\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\right\}$
50 coeq1 ${⊢}{m}={Q}\to {m}\circ {A}={Q}\circ {A}$
51 50 eqeq1d ${⊢}{m}={Q}\to \left({m}\circ {A}={X}↔{Q}\circ {A}={X}\right)$
52 coeq1 ${⊢}{m}={Q}\to {m}\circ {V}={Q}\circ {V}$
53 52 eqeq1d ${⊢}{m}={Q}\to \left({m}\circ {V}={Y}↔{Q}\circ {V}={Y}\right)$
54 51 53 anbi12d ${⊢}{m}={Q}\to \left(\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)↔\left({Q}\circ {A}={X}\wedge {Q}\circ {V}={Y}\right)\right)$
55 54 elrab ${⊢}{Q}\in \left\{{m}\in \left({W}\mathrm{RingHom}{T}\right)|\left({m}\circ {A}={X}\wedge {m}\circ {V}={Y}\right)\right\}↔\left({Q}\in \left({W}\mathrm{RingHom}{T}\right)\wedge \left({Q}\circ {A}={X}\wedge {Q}\circ {V}={Y}\right)\right)$
56 49 55 sylib ${⊢}\left({I}\in {Z}\wedge {S}\in \mathrm{CRing}\wedge {R}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({Q}\in \left({W}\mathrm{RingHom}{T}\right)\wedge \left({Q}\circ {A}={X}\wedge {Q}\circ {V}={Y}\right)\right)$