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

Metamath Proof Explorer

Theorem ply1plusgpropd

Description: Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses ply1baspropd.b1 
|- ( ph -> B = ( Base ` R ) )
ply1baspropd.b2 
|- ( ph -> B = ( Base ` S ) )
ply1baspropd.p 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
Assertion ply1plusgpropd 
|- ( ph -> ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` S ) ) )

Proof

Step Hyp Ref Expression
1 ply1baspropd.b1 
 |-  ( ph -> B = ( Base ` R ) )
2 ply1baspropd.b2 
 |-  ( ph -> B = ( Base ` S ) )
3 ply1baspropd.p 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
4 1 2 3 psrplusgpropd 
 |-  ( ph -> ( +g ` ( 1o mPwSer R ) ) = ( +g ` ( 1o mPwSer S ) ) )
5 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
6 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
7 eqid 
 |-  ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPoly R ) )
8 5 6 7 mplplusg 
 |-  ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPwSer R ) )
9 eqid 
 |-  ( 1o mPoly S ) = ( 1o mPoly S )
10 eqid 
 |-  ( 1o mPwSer S ) = ( 1o mPwSer S )
11 eqid 
 |-  ( +g ` ( 1o mPoly S ) ) = ( +g ` ( 1o mPoly S ) )
12 9 10 11 mplplusg 
 |-  ( +g ` ( 1o mPoly S ) ) = ( +g ` ( 1o mPwSer S ) )
13 4 8 12 3eqtr4g 
 |-  ( ph -> ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPoly S ) ) )
14 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
15 eqid 
 |-  ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` R ) )
16 14 5 15 ply1plusg 
 |-  ( +g ` ( Poly1 ` R ) ) = ( +g ` ( 1o mPoly R ) )
17 eqid 
 |-  ( Poly1 ` S ) = ( Poly1 ` S )
18 eqid 
 |-  ( +g ` ( Poly1 ` S ) ) = ( +g ` ( Poly1 ` S ) )
19 17 9 18 ply1plusg 
 |-  ( +g ` ( Poly1 ` S ) ) = ( +g ` ( 1o mPoly S ) )
20 13 16 19 3eqtr4g 
 |-  ( ph -> ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` S ) ) )