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

Metamath Proof Explorer

Theorem ply1vsca

Description: Value of scalar multiplication 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 
|- Y = ( Poly1 ` R )
ply1plusg.s 
|- S = ( 1o mPoly R )
ply1vscafval.n 
|- .x. = ( .s ` Y )
Assertion ply1vsca 
|- .x. = ( .s ` S )

Proof

Step Hyp Ref Expression
1 ply1plusg.y 
 |-  Y = ( Poly1 ` R )
2 ply1plusg.s 
 |-  S = ( 1o mPoly R )
3 ply1vscafval.n 
 |-  .x. = ( .s ` Y )
4 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
5 eqid 
 |-  ( .s ` S ) = ( .s ` S )
6 2 4 5 mplvsca2 
 |-  ( .s ` S ) = ( .s ` ( 1o mPwSer R ) )
7 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
8 eqid 
 |-  ( .s ` ( PwSer1 ` R ) ) = ( .s ` ( PwSer1 ` R ) )
9 7 4 8 psr1vsca 
 |-  ( .s ` ( PwSer1 ` R ) ) = ( .s ` ( 1o mPwSer R ) )
10 fvex 
 |-  ( Base ` ( 1o mPoly R ) ) e. _V
11 1 7 ply1val 
 |-  Y = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
12 11 8 ressvsca 
 |-  ( ( Base ` ( 1o mPoly R ) ) e. _V -> ( .s ` ( PwSer1 ` R ) ) = ( .s ` Y ) )
13 10 12 ax-mp 
 |-  ( .s ` ( PwSer1 ` R ) ) = ( .s ` Y )
14 6 9 13 3eqtr2i 
 |-  ( .s ` S ) = ( .s ` Y )
15 3 14 eqtr4i 
 |-  .x. = ( .s ` S )