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=IevalSubSR
evlsval.w W=ImPolyU
evlsval.v V=ImVarU
evlsval.u U=S𝑠R
evlsval.t T=S𝑠BI
evlsval.b B=BaseS
evlsval.a A=algScW
evlsval.x X=xRBI×x
evlsval.y Y=xIgBIgx
Assertion evlsval IZSCRingRSubRingSQ=ιfWRingHomT|fA=XfV=Y

Proof

Step Hyp Ref Expression
1 evlsval.q Q=IevalSubSR
2 evlsval.w W=ImPolyU
3 evlsval.v V=ImVarU
4 evlsval.u U=S𝑠R
5 evlsval.t T=S𝑠BI
6 evlsval.b B=BaseS
7 evlsval.a A=algScW
8 evlsval.x X=xRBI×x
9 evlsval.y Y=xIgBIgx
10 elex IZIV
11 fveq2 s=SBases=BaseS
12 11 adantl i=Is=SBases=BaseS
13 12 csbeq1d i=Is=SBases/brSubRingsimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=BaseS/brSubRingsimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx
14 fvex BaseSV
15 14 a1i i=Is=SBaseSV
16 simplr i=Is=Sb=BaseSs=S
17 16 fveq2d i=Is=Sb=BaseSSubRings=SubRingS
18 simpll i=Is=Sb=BaseSi=I
19 oveq1 s=Ss𝑠r=S𝑠r
20 19 ad2antlr i=Is=Sb=BaseSs𝑠r=S𝑠r
21 18 20 oveq12d i=Is=Sb=BaseSimPolys𝑠r=ImPolyS𝑠r
22 21 csbeq1d i=Is=Sb=BaseSimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=ImPolyS𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx
23 ovexd i=Is=Sb=BaseSImPolyS𝑠rV
24 simprr i=Is=Sb=BaseSw=ImPolyS𝑠rw=ImPolyS𝑠r
25 simplr i=Is=Sb=BaseSw=ImPolyS𝑠rs=S
26 simprl i=Is=Sb=BaseSw=ImPolyS𝑠rb=BaseS
27 simpll i=Is=Sb=BaseSw=ImPolyS𝑠ri=I
28 26 27 oveq12d i=Is=Sb=BaseSw=ImPolyS𝑠rbi=BaseSI
29 25 28 oveq12d i=Is=Sb=BaseSw=ImPolyS𝑠rs𝑠bi=S𝑠BaseSI
30 24 29 oveq12d i=Is=Sb=BaseSw=ImPolyS𝑠rwRingHoms𝑠bi=ImPolyS𝑠rRingHomS𝑠BaseSI
31 24 fveq2d i=Is=Sb=BaseSw=ImPolyS𝑠ralgScw=algScImPolyS𝑠r
32 31 coeq2d i=Is=Sb=BaseSw=ImPolyS𝑠rfalgScw=falgScImPolyS𝑠r
33 28 xpeq1d i=Is=Sb=BaseSw=ImPolyS𝑠rbi×x=BaseSI×x
34 33 mpteq2dv i=Is=Sb=BaseSw=ImPolyS𝑠rxrbi×x=xrBaseSI×x
35 32 34 eqeq12d i=Is=Sb=BaseSw=ImPolyS𝑠rfalgScw=xrbi×xfalgScImPolyS𝑠r=xrBaseSI×x
36 25 oveq1d i=Is=Sb=BaseSw=ImPolyS𝑠rs𝑠r=S𝑠r
37 27 36 oveq12d i=Is=Sb=BaseSw=ImPolyS𝑠rimVars𝑠r=ImVarS𝑠r
38 37 coeq2d i=Is=Sb=BaseSw=ImPolyS𝑠rfimVars𝑠r=fImVarS𝑠r
39 28 mpteq1d i=Is=Sb=BaseSw=ImPolyS𝑠rgbigx=gBaseSIgx
40 27 39 mpteq12dv i=Is=Sb=BaseSw=ImPolyS𝑠rxigbigx=xIgBaseSIgx
41 38 40 eqeq12d i=Is=Sb=BaseSw=ImPolyS𝑠rfimVars𝑠r=xigbigxfImVarS𝑠r=xIgBaseSIgx
42 35 41 anbi12d i=Is=Sb=BaseSw=ImPolyS𝑠rfalgScw=xrbi×xfimVars𝑠r=xigbigxfalgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
43 30 42 riotaeqbidv i=Is=Sb=BaseSw=ImPolyS𝑠rιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=ιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
44 43 anassrs i=Is=Sb=BaseSw=ImPolyS𝑠rιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=ιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
45 23 44 csbied i=Is=Sb=BaseSImPolyS𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=ιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
46 22 45 eqtrd i=Is=Sb=BaseSimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=ιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
47 17 46 mpteq12dv i=Is=Sb=BaseSrSubRingsimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
48 15 47 csbied i=Is=SBaseS/brSubRingsimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
49 13 48 eqtrd i=Is=SBases/brSubRingsimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
50 df-evls evalSub=iV,sCRingBases/brSubRingsimPolys𝑠r/wιfwRingHoms𝑠bi|falgScw=xrbi×xfimVars𝑠r=xigbigx
51 fvex SubRingSV
52 51 mptex rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxV
53 49 50 52 ovmpoa IVSCRingIevalSubS=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
54 53 fveq1d IVSCRingIevalSubSR=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxR
55 10 54 sylan IZSCRingIevalSubSR=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxR
56 1 55 eqtrid IZSCRingQ=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxR
57 56 3adant3 IZSCRingRSubRingSQ=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxR
58 oveq2 r=RS𝑠r=S𝑠R
59 58 oveq2d r=RImPolyS𝑠r=ImPolyS𝑠R
60 59 oveq1d r=RImPolyS𝑠rRingHomS𝑠BaseSI=ImPolyS𝑠RRingHomS𝑠BaseSI
61 59 fveq2d r=RalgScImPolyS𝑠r=algScImPolyS𝑠R
62 61 coeq2d r=RfalgScImPolyS𝑠r=falgScImPolyS𝑠R
63 mpteq1 r=RxrBaseSI×x=xRBaseSI×x
64 62 63 eqeq12d r=RfalgScImPolyS𝑠r=xrBaseSI×xfalgScImPolyS𝑠R=xRBaseSI×x
65 58 oveq2d r=RImVarS𝑠r=ImVarS𝑠R
66 65 coeq2d r=RfImVarS𝑠r=fImVarS𝑠R
67 66 eqeq1d r=RfImVarS𝑠r=xIgBaseSIgxfImVarS𝑠R=xIgBaseSIgx
68 64 67 anbi12d r=RfalgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxfalgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgx
69 60 68 riotaeqbidv r=RιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx=ιfImPolyS𝑠RRingHomS𝑠BaseSI|falgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgx
70 eqid rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx=rSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgx
71 riotaex ιfImPolyS𝑠RRingHomS𝑠BaseSI|falgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgxV
72 69 70 71 fvmpt RSubRingSrSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxR=ιfImPolyS𝑠RRingHomS𝑠BaseSI|falgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgx
73 4 oveq2i ImPolyU=ImPolyS𝑠R
74 2 73 eqtri W=ImPolyS𝑠R
75 6 oveq1i BI=BaseSI
76 75 oveq2i S𝑠BI=S𝑠BaseSI
77 5 76 eqtri T=S𝑠BaseSI
78 74 77 oveq12i WRingHomT=ImPolyS𝑠RRingHomS𝑠BaseSI
79 78 a1i WRingHomT=ImPolyS𝑠RRingHomS𝑠BaseSI
80 74 fveq2i algScW=algScImPolyS𝑠R
81 7 80 eqtri A=algScImPolyS𝑠R
82 81 coeq2i fA=falgScImPolyS𝑠R
83 75 xpeq1i BI×x=BaseSI×x
84 83 mpteq2i xRBI×x=xRBaseSI×x
85 8 84 eqtri X=xRBaseSI×x
86 82 85 eqeq12i fA=XfalgScImPolyS𝑠R=xRBaseSI×x
87 4 oveq2i ImVarU=ImVarS𝑠R
88 3 87 eqtri V=ImVarS𝑠R
89 88 coeq2i fV=fImVarS𝑠R
90 eqid gx=gx
91 75 90 mpteq12i gBIgx=gBaseSIgx
92 91 mpteq2i xIgBIgx=xIgBaseSIgx
93 9 92 eqtri Y=xIgBaseSIgx
94 89 93 eqeq12i fV=YfImVarS𝑠R=xIgBaseSIgx
95 86 94 anbi12i fA=XfV=YfalgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgx
96 95 a1i fA=XfV=YfalgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgx
97 79 96 riotaeqbidv ιfWRingHomT|fA=XfV=Y=ιfImPolyS𝑠RRingHomS𝑠BaseSI|falgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgx
98 97 mptru ιfWRingHomT|fA=XfV=Y=ιfImPolyS𝑠RRingHomS𝑠BaseSI|falgScImPolyS𝑠R=xRBaseSI×xfImVarS𝑠R=xIgBaseSIgx
99 72 98 eqtr4di RSubRingSrSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxR=ιfWRingHomT|fA=XfV=Y
100 99 3ad2ant3 IZSCRingRSubRingSrSubRingSιfImPolyS𝑠rRingHomS𝑠BaseSI|falgScImPolyS𝑠r=xrBaseSI×xfImVarS𝑠r=xIgBaseSIgxR=ιfWRingHomT|fA=XfV=Y
101 57 100 eqtrd IZSCRingRSubRingSQ=ιfWRingHomT|fA=XfV=Y