Theorem mplvsca2

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

	Ref	Expression
Hypotheses	mplvsca2.p	$$⊢P=I\mathrm{mPoly}R$$
	mplvsca2.s	$$⊢S=I\mathrm{mPwSer}R$$
	mplvsca2.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
Assertion	mplvsca2	$$⊢\underset{\dot{}}{·}={\cdot }_S$$

Proof

Step	Hyp	Ref	Expression
1		mplvsca2.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplvsca2.s	$$⊢S=I\mathrm{mPwSer}R$$
3		mplvsca2.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
4		fvex	$$⊢{\mathrm{Base}}_P\in \mathrm{V}$$
5		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
6	1 2 5	mplval2	$$⊢P=S{\upharpoonright }_{𝑠}{\mathrm{Base}}_P$$
7		eqid	$$⊢{\cdot }_S={\cdot }_S$$
8	6 7	ressvsca	$$⊢{\mathrm{Base}}_P\in \mathrm{V}\to {\cdot }_S={\cdot }_P$$
9	4 8	ax-mp	$$⊢{\cdot }_S={\cdot }_P$$
10	3 9	eqtr4i	$$⊢\underset{\dot{}}{·}={\cdot }_S$$