Description: Value of addition in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ply1plusg.y | |
|
ply1plusg.s | |
||
ply1plusg.p | |
||
Assertion | ply1plusg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1plusg.y | |
|
2 | ply1plusg.s | |
|
3 | ply1plusg.p | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 2 4 5 | mplplusg | |
7 | eqid | |
|
8 | eqid | |
|
9 | 7 4 8 | psr1plusg | |
10 | fvex | |
|
11 | 1 7 | ply1val | |
12 | 11 8 | ressplusg | |
13 | 10 12 | ax-mp | |
14 | 6 9 13 | 3eqtr2i | |
15 | 3 14 | eqtr4i | |