Theorem ply1plusgpropd

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

	Ref	Expression
Hypotheses	ply1baspropd.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	ply1baspropd.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
	ply1baspropd.p	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
Assertion	ply1plusgpropd	⊢ ( 𝜑 → ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( Poly1 ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1baspropd.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2		ply1baspropd.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
3		ply1baspropd.p	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
4	1 2 3	psrplusgpropd	⊢ ( 𝜑 → ( +g ‘ ( 1o mPwSer 𝑅 ) ) = ( +g ‘ ( 1o mPwSer 𝑆 ) ) )
5		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
7		eqid	⊢ ( +g ‘ ( 1o mPoly 𝑅 ) ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
8	5 6 7	mplplusg	⊢ ( +g ‘ ( 1o mPoly 𝑅 ) ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
9		eqid	⊢ ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
10		eqid	⊢ ( 1o mPwSer 𝑆 ) = ( 1o mPwSer 𝑆 )
11		eqid	⊢ ( +g ‘ ( 1o mPoly 𝑆 ) ) = ( +g ‘ ( 1o mPoly 𝑆 ) )
12	9 10 11	mplplusg	⊢ ( +g ‘ ( 1o mPoly 𝑆 ) ) = ( +g ‘ ( 1o mPwSer 𝑆 ) )
13	4 8 12	3eqtr4g	⊢ ( 𝜑 → ( +g ‘ ( 1o mPoly 𝑅 ) ) = ( +g ‘ ( 1o mPoly 𝑆 ) ) )
14		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
15		eqid	⊢ ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( Poly1 ‘ 𝑅 ) )
16	14 5 15	ply1plusg	⊢ ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
17		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
18		eqid	⊢ ( +g ‘ ( Poly1 ‘ 𝑆 ) ) = ( +g ‘ ( Poly1 ‘ 𝑆 ) )
19	17 9 18	ply1plusg	⊢ ( +g ‘ ( Poly1 ‘ 𝑆 ) ) = ( +g ‘ ( 1o mPoly 𝑆 ) )
20	13 16 19	3eqtr4g	⊢ ( 𝜑 → ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( Poly1 ‘ 𝑆 ) ) )