Metamath Proof Explorer


Theorem ply1plusg

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 Y=Poly1R
ply1plusg.s S=1𝑜mPolyR
ply1plusg.p +˙=+Y
Assertion ply1plusg +˙=+S

Proof

Step Hyp Ref Expression
1 ply1plusg.y Y=Poly1R
2 ply1plusg.s S=1𝑜mPolyR
3 ply1plusg.p +˙=+Y
4 eqid 1𝑜mPwSerR=1𝑜mPwSerR
5 eqid +S=+S
6 2 4 5 mplplusg +S=+1𝑜mPwSerR
7 eqid PwSer1R=PwSer1R
8 eqid +PwSer1R=+PwSer1R
9 7 4 8 psr1plusg +PwSer1R=+1𝑜mPwSerR
10 fvex Base1𝑜mPolyRV
11 1 7 ply1val Y=PwSer1R𝑠Base1𝑜mPolyR
12 11 8 ressplusg Base1𝑜mPolyRV+PwSer1R=+Y
13 10 12 ax-mp +PwSer1R=+Y
14 6 9 13 3eqtr2i +S=+Y
15 3 14 eqtr4i +˙=+S