Description: Univariate polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | evls1pw.q | |
|
evls1pw.u | |
||
evls1pw.w | |
||
evls1pw.g | |
||
evls1pw.k | |
||
evls1pw.b | |
||
evls1pw.e | |
||
evls1pw.s | |
||
evls1pw.r | |
||
evls1pw.n | |
||
evls1pw.x | |
||
Assertion | evls1pw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evls1pw.q | |
|
2 | evls1pw.u | |
|
3 | evls1pw.w | |
|
4 | evls1pw.g | |
|
5 | evls1pw.k | |
|
6 | evls1pw.b | |
|
7 | evls1pw.e | |
|
8 | evls1pw.s | |
|
9 | evls1pw.r | |
|
10 | evls1pw.n | |
|
11 | evls1pw.x | |
|
12 | eqid | |
|
13 | 1 5 12 2 3 | evls1rhm | |
14 | 8 9 13 | syl2anc | |
15 | eqid | |
|
16 | 4 15 | rhmmhm | |
17 | 14 16 | syl | |
18 | 4 6 | mgpbas | |
19 | eqid | |
|
20 | 18 7 19 | mhmmulg | |
21 | 17 10 11 20 | syl3anc | |