This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Poly1 ` R )
ply1plusg.s 
|- S = ( 1o mPoly R )
ply1plusg.p 
|- .+ = ( +g ` Y )
Assertion ply1plusg 
|- .+ = ( +g ` S )

Proof

Step Hyp Ref Expression
1 ply1plusg.y 
 |-  Y = ( Poly1 ` R )
2 ply1plusg.s 
 |-  S = ( 1o mPoly R )
3 ply1plusg.p 
 |-  .+ = ( +g ` Y )
4 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
5 eqid 
 |-  ( +g ` S ) = ( +g ` S )
6 2 4 5 mplplusg 
 |-  ( +g ` S ) = ( +g ` ( 1o mPwSer R ) )
7 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
8 eqid 
 |-  ( +g ` ( PwSer1 ` R ) ) = ( +g ` ( PwSer1 ` R ) )
9 7 4 8 psr1plusg 
 |-  ( +g ` ( PwSer1 ` R ) ) = ( +g ` ( 1o mPwSer R ) )
10 fvex 
 |-  ( Base ` ( 1o mPoly R ) ) e. _V
11 1 7 ply1val 
 |-  Y = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
12 11 8 ressplusg 
 |-  ( ( Base ` ( 1o mPoly R ) ) e. _V -> ( +g ` ( PwSer1 ` R ) ) = ( +g ` Y ) )
13 10 12 ax-mp 
 |-  ( +g ` ( PwSer1 ` R ) ) = ( +g ` Y )
14 6 9 13 3eqtr2i 
 |-  ( +g ` S ) = ( +g ` Y )
15 3 14 eqtr4i 
 |-  .+ = ( +g ` S )