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 ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
ply1plusg.s ⊢ 𝑆 = ( 1o mPoly 𝑅 )
ply1plusg.p ⊢ + = ( +g ‘ 𝑌 )
Assertion ply1plusg + = ( +g ‘ 𝑆 )

Proof

Step Hyp Ref Expression
1 ply1plusg.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 ply1plusg.s ⊢ 𝑆 = ( 1o mPoly 𝑅 )
3 ply1plusg.p ⊢ + = ( +g ‘ 𝑌 )
4 eqid ⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
6 2 4 5 mplplusg ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
7 eqid ⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
8 eqid ⊢ ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ ( PwSer1 ‘ 𝑅 ) )
9 7 4 8 psr1plusg ⊢ ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
10 fvex ⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V
11 1 7 ply1val ⊢ 𝑌 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
12 11 8 ressplusg ⊢ ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V → ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ 𝑌 ) )
13 10 12 ax-mp ⊢ ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ 𝑌 )
14 6 9 13 3eqtr2i ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑌 )
15 3 14 eqtr4i ⊢ + = ( +g ‘ 𝑆 )