Description: Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | evlsval3.q | |
|
evlsval3.p | |
||
evlsval3.b | |
||
evlsval3.d | |
||
evlsval3.k | |
||
evlsval3.u | |
||
evlsval3.t | |
||
evlsval3.m | |
||
evlsval3.w | |
||
evlsval3.x | |
||
evlsval3.e | |
||
evlsval3.f | |
||
evlsval3.g | |
||
evlsval3.i | |
||
evlsval3.s | |
||
evlsval3.r | |
||
Assertion | evlsval3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evlsval3.q | |
|
2 | evlsval3.p | |
|
3 | evlsval3.b | |
|
4 | evlsval3.d | |
|
5 | evlsval3.k | |
|
6 | evlsval3.u | |
|
7 | evlsval3.t | |
|
8 | evlsval3.m | |
|
9 | evlsval3.w | |
|
10 | evlsval3.x | |
|
11 | evlsval3.e | |
|
12 | evlsval3.f | |
|
13 | evlsval3.g | |
|
14 | evlsval3.i | |
|
15 | evlsval3.s | |
|
16 | evlsval3.r | |
|
17 | eqid | |
|
18 | eqid | |
|
19 | 1 2 17 6 7 5 18 12 13 | evlsval | |
20 | 14 15 16 19 | syl3anc | |
21 | eqid | |
|
22 | 6 | subrgcrng | |
23 | 15 16 22 | syl2anc | |
24 | ovexd | |
|
25 | 7 | pwscrng | |
26 | 15 24 25 | syl2anc | |
27 | 5 | subrgss | |
28 | 16 27 | syl | |
29 | 28 | resmptd | |
30 | 12 29 | eqtr4id | |
31 | 15 | crngringd | |
32 | eqid | |
|
33 | 7 5 32 | pwsdiagrhm | |
34 | 31 24 33 | syl2anc | |
35 | 6 | resrhm | |
36 | 34 16 35 | syl2anc | |
37 | 30 36 | eqeltrd | |
38 | 5 | fvexi | |
39 | elmapg | |
|
40 | 38 14 39 | sylancr | |
41 | 40 | biimpa | |
42 | 41 | adantlr | |
43 | simplr | |
|
44 | 42 43 | ffvelrnd | |
45 | 44 | fmpttd | |
46 | ovexd | |
|
47 | 7 5 21 | pwselbasb | |
48 | 15 46 47 | syl2an2r | |
49 | 45 48 | mpbird | |
50 | 49 13 | fmptd | |
51 | 2 3 21 4 8 9 10 17 11 14 23 26 37 50 18 | evlslem1 | |
52 | 51 | simp2d | |
53 | 51 | simp3d | |
54 | 51 | simp1d | |
55 | 2 21 18 17 14 23 26 37 50 | evlseu | |
56 | coeq1 | |
|
57 | 56 | eqeq1d | |
58 | coeq1 | |
|
59 | 58 | eqeq1d | |
60 | 57 59 | anbi12d | |
61 | 60 | riota2 | |
62 | 54 55 61 | syl2anc | |
63 | 52 53 62 | mpbi2and | |
64 | 20 63 | eqtrd | |