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 ) ) )