Metamath Proof Explorer


Theorem evlsval3

Description: Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024)

Ref Expression
Hypotheses evlsval3.q Q=IevalSubSR
evlsval3.p P=ImPolyU
evlsval3.b B=BaseP
evlsval3.d D=h0I|h-1Fin
evlsval3.k K=BaseS
evlsval3.u U=S𝑠R
evlsval3.t T=S𝑠KI
evlsval3.m M=mulGrpT
evlsval3.w ×˙=M
evlsval3.x ·˙=T
evlsval3.e E=pBTbDFpb·˙Mb×˙fG
evlsval3.f F=xRKI×x
evlsval3.g G=xIaKIax
evlsval3.i φIV
evlsval3.s φSCRing
evlsval3.r φRSubRingS
Assertion evlsval3 φQ=E

Proof

Step Hyp Ref Expression
1 evlsval3.q Q=IevalSubSR
2 evlsval3.p P=ImPolyU
3 evlsval3.b B=BaseP
4 evlsval3.d D=h0I|h-1Fin
5 evlsval3.k K=BaseS
6 evlsval3.u U=S𝑠R
7 evlsval3.t T=S𝑠KI
8 evlsval3.m M=mulGrpT
9 evlsval3.w ×˙=M
10 evlsval3.x ·˙=T
11 evlsval3.e E=pBTbDFpb·˙Mb×˙fG
12 evlsval3.f F=xRKI×x
13 evlsval3.g G=xIaKIax
14 evlsval3.i φIV
15 evlsval3.s φSCRing
16 evlsval3.r φRSubRingS
17 eqid ImVarU=ImVarU
18 eqid algScP=algScP
19 1 2 17 6 7 5 18 12 13 evlsval IVSCRingRSubRingSQ=ιfPRingHomT|falgScP=FfImVarU=G
20 14 15 16 19 syl3anc φQ=ιfPRingHomT|falgScP=FfImVarU=G
21 eqid BaseT=BaseT
22 6 subrgcrng SCRingRSubRingSUCRing
23 15 16 22 syl2anc φUCRing
24 ovexd φKIV
25 7 pwscrng SCRingKIVTCRing
26 15 24 25 syl2anc φTCRing
27 5 subrgss RSubRingSRK
28 16 27 syl φRK
29 28 resmptd φxKKI×xR=xRKI×x
30 12 29 eqtr4id φF=xKKI×xR
31 15 crngringd φSRing
32 eqid xKKI×x=xKKI×x
33 7 5 32 pwsdiagrhm SRingKIVxKKI×xSRingHomT
34 31 24 33 syl2anc φxKKI×xSRingHomT
35 6 resrhm xKKI×xSRingHomTRSubRingSxKKI×xRURingHomT
36 34 16 35 syl2anc φxKKI×xRURingHomT
37 30 36 eqeltrd φFURingHomT
38 5 fvexi KV
39 elmapg KVIVaKIa:IK
40 38 14 39 sylancr φaKIa:IK
41 40 biimpa φaKIa:IK
42 41 adantlr φxIaKIa:IK
43 simplr φxIaKIxI
44 42 43 ffvelrnd φxIaKIaxK
45 44 fmpttd φxIaKIax:KIK
46 ovexd φxIKIV
47 7 5 21 pwselbasb SCRingKIVaKIaxBaseTaKIax:KIK
48 15 46 47 syl2an2r φxIaKIaxBaseTaKIax:KIK
49 45 48 mpbird φxIaKIaxBaseT
50 49 13 fmptd φG:IBaseT
51 2 3 21 4 8 9 10 17 11 14 23 26 37 50 18 evlslem1 φEPRingHomTEalgScP=FEImVarU=G
52 51 simp2d φEalgScP=F
53 51 simp3d φEImVarU=G
54 51 simp1d φEPRingHomT
55 2 21 18 17 14 23 26 37 50 evlseu φ∃!fPRingHomTfalgScP=FfImVarU=G
56 coeq1 f=EfalgScP=EalgScP
57 56 eqeq1d f=EfalgScP=FEalgScP=F
58 coeq1 f=EfImVarU=EImVarU
59 58 eqeq1d f=EfImVarU=GEImVarU=G
60 57 59 anbi12d f=EfalgScP=FfImVarU=GEalgScP=FEImVarU=G
61 60 riota2 EPRingHomT∃!fPRingHomTfalgScP=FfImVarU=GEalgScP=FEImVarU=GιfPRingHomT|falgScP=FfImVarU=G=E
62 54 55 61 syl2anc φEalgScP=FEImVarU=GιfPRingHomT|falgScP=FfImVarU=G=E
63 52 53 62 mpbi2and φιfPRingHomT|falgScP=FfImVarU=G=E
64 20 63 eqtrd φQ=E