Description: Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | evl1fval1.q | |
|
evl1fval1.b | |
||
Assertion | evl1fval1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evl1fval1.q | |
|
2 | evl1fval1.b | |
|
3 | 1 2 | evl1fval1lem | |
4 | fvprc | |
|
5 | 1 4 | eqtrid | |
6 | reldmevls1 | |
|
7 | 6 | ovprc1 | |
8 | 5 7 | eqtr4d | |
9 | 3 8 | pm2.61i | |