Theorem mplvsca2

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mplvsca2.p	|- P = ( I mPoly R )
	mplvsca2.s	|- S = ( I mPwSer R )
	mplvsca2.n	|- .x. = ( .s ` P )
Assertion	mplvsca2	|- .x. = ( .s ` S )

Proof

Step	Hyp	Ref	Expression
1		mplvsca2.p	|- P = ( I mPoly R )
2		mplvsca2.s	|- S = ( I mPwSer R )
3		mplvsca2.n	|- .x. = ( .s ` P )
4		fvex	|- ( Base ` P ) e. _V
5		eqid	|- ( Base ` P ) = ( Base ` P )
6	1 2 5	mplval2	|- P = ( S |`s ( Base ` P ) )
7		eqid	|- ( .s ` S ) = ( .s ` S )
8	6 7	ressvsca	|- ( ( Base ` P ) e. _V -> ( .s ` S ) = ( .s ` P ) )
9	4 8	ax-mp	|- ( .s ` S ) = ( .s ` P )
10	3 9	eqtr4i	|- .x. = ( .s ` S )