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 = I evalSub S R
evlsval3.p P = I mPoly U
evlsval3.b B = Base P
evlsval3.d D = h 0 I | h -1 Fin
evlsval3.k K = Base S
evlsval3.u U = S 𝑠 R
evlsval3.t T = S 𝑠 K I
evlsval3.m M = mulGrp T
evlsval3.w × ˙ = M
evlsval3.x · ˙ = T
evlsval3.e E = p B T b D F p b · ˙ M b × ˙ f G
evlsval3.f F = x R K I × x
evlsval3.g G = x I a K I a x
evlsval3.i φ I V
evlsval3.s φ S CRing
evlsval3.r φ R SubRing S
Assertion evlsval3 φ Q = E

Proof

Step Hyp Ref Expression
1 evlsval3.q Q = I evalSub S R
2 evlsval3.p P = I mPoly U
3 evlsval3.b B = Base P
4 evlsval3.d D = h 0 I | h -1 Fin
5 evlsval3.k K = Base S
6 evlsval3.u U = S 𝑠 R
7 evlsval3.t T = S 𝑠 K I
8 evlsval3.m M = mulGrp T
9 evlsval3.w × ˙ = M
10 evlsval3.x · ˙ = T
11 evlsval3.e E = p B T b D F p b · ˙ M b × ˙ f G
12 evlsval3.f F = x R K I × x
13 evlsval3.g G = x I a K I a x
14 evlsval3.i φ I V
15 evlsval3.s φ S CRing
16 evlsval3.r φ R SubRing S
17 eqid I mVar U = I mVar U
18 eqid algSc P = algSc P
19 1 2 17 6 7 5 18 12 13 evlsval I V S CRing R SubRing S Q = ι f P RingHom T | f algSc P = F f I mVar U = G
20 14 15 16 19 syl3anc φ Q = ι f P RingHom T | f algSc P = F f I mVar U = G
21 eqid Base T = Base T
22 6 subrgcrng S CRing R SubRing S U CRing
23 15 16 22 syl2anc φ U CRing
24 ovexd φ K I V
25 7 pwscrng S CRing K I V T CRing
26 15 24 25 syl2anc φ T CRing
27 5 subrgss R SubRing S R K
28 16 27 syl φ R K
29 28 resmptd φ x K K I × x R = x R K I × x
30 12 29 eqtr4id φ F = x K K I × x R
31 15 crngringd φ S Ring
32 eqid x K K I × x = x K K I × x
33 7 5 32 pwsdiagrhm S Ring K I V x K K I × x S RingHom T
34 31 24 33 syl2anc φ x K K I × x S RingHom T
35 6 resrhm x K K I × x S RingHom T R SubRing S x K K I × x R U RingHom T
36 34 16 35 syl2anc φ x K K I × x R U RingHom T
37 30 36 eqeltrd φ F U RingHom T
38 5 fvexi K V
39 elmapg K V I V a K I a : I K
40 38 14 39 sylancr φ a K I a : I K
41 40 biimpa φ a K I a : I K
42 41 adantlr φ x I a K I a : I K
43 simplr φ x I a K I x I
44 42 43 ffvelrnd φ x I a K I a x K
45 44 fmpttd φ x I a K I a x : K I K
46 ovexd φ x I K I V
47 7 5 21 pwselbasb S CRing K I V a K I a x Base T a K I a x : K I K
48 15 46 47 syl2an2r φ x I a K I a x Base T a K I a x : K I K
49 45 48 mpbird φ x I a K I a x Base T
50 49 13 fmptd φ G : I Base T
51 2 3 21 4 8 9 10 17 11 14 23 26 37 50 18 evlslem1 φ E P RingHom T E algSc P = F E I mVar U = G
52 51 simp2d φ E algSc P = F
53 51 simp3d φ E I mVar U = G
54 51 simp1d φ E P RingHom T
55 2 21 18 17 14 23 26 37 50 evlseu φ ∃! f P RingHom T f algSc P = F f I mVar U = G
56 coeq1 f = E f algSc P = E algSc P
57 56 eqeq1d f = E f algSc P = F E algSc P = F
58 coeq1 f = E f I mVar U = E I mVar U
59 58 eqeq1d f = E f I mVar U = G E I mVar U = G
60 57 59 anbi12d f = E f algSc P = F f I mVar U = G E algSc P = F E I mVar U = G
61 60 riota2 E P RingHom T ∃! f P RingHom T f algSc P = F f I mVar U = G E algSc P = F E I mVar U = G ι f P RingHom T | f algSc P = F f I mVar U = G = E
62 54 55 61 syl2anc φ E algSc P = F E I mVar U = G ι f P RingHom T | f algSc P = F f I mVar U = G = E
63 52 53 62 mpbi2and φ ι f P RingHom T | f algSc P = F f I mVar U = G = E
64 20 63 eqtrd φ Q = E