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 )