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 ⊢ ( 𝜑 → 𝐵 = ( 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 ‘ 𝑆 ) ) )