# 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 𝑌 = ( Poly1𝑅 )
ply1plusg.s 𝑆 = ( 1o mPoly 𝑅 )
ply1plusg.p + = ( +g𝑌 )
Assertion ply1plusg + = ( +g𝑆 )

### Proof

Step Hyp Ref Expression
1 ply1plusg.y 𝑌 = ( Poly1𝑅 )
2 ply1plusg.s 𝑆 = ( 1o mPoly 𝑅 )
3 ply1plusg.p + = ( +g𝑌 )
4 eqid ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5 eqid ( +g𝑆 ) = ( +g𝑆 )
6 2 4 5 mplplusg ( +g𝑆 ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
7 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
8 eqid ( +g ‘ ( PwSer1𝑅 ) ) = ( +g ‘ ( PwSer1𝑅 ) )
9 7 4 8 psr1plusg ( +g ‘ ( PwSer1𝑅 ) ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
10 fvex ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V
11 1 7 ply1val 𝑌 = ( ( PwSer1𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
12 11 8 ressplusg ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V → ( +g ‘ ( PwSer1𝑅 ) ) = ( +g𝑌 ) )
13 10 12 ax-mp ( +g ‘ ( PwSer1𝑅 ) ) = ( +g𝑌 )
14 6 9 13 3eqtr2i ( +g𝑆 ) = ( +g𝑌 )
15 3 14 eqtr4i + = ( +g𝑆 )