Theorem mplvsca

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

	Ref	Expression
Hypotheses	mplvsca.p	$$⊢P=I\mathrm{mPoly}R$$
	mplvsca.n	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	mplvsca.k	$$⊢K={\mathrm{Base}}_R$$
	mplvsca.b	$$⊢B={\mathrm{Base}}_P$$
	mplvsca.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mplvsca.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplvsca.x	$$⊢\phi \to X\in K$$
	mplvsca.f	$$⊢\phi \to F\in B$$
Assertion	mplvsca	$$⊢\phi \to X\underset{\dot{}}{\bullet }F=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$

Proof

Step	Hyp	Ref	Expression
1		mplvsca.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplvsca.n	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
3		mplvsca.k	$$⊢K={\mathrm{Base}}_R$$
4		mplvsca.b	$$⊢B={\mathrm{Base}}_P$$
5		mplvsca.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		mplvsca.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
7		mplvsca.x	$$⊢\phi \to X\in K$$
8		mplvsca.f	$$⊢\phi \to F\in B$$
9		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
10	1 9 2	mplvsca2	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(I\mathrm{mPwSer}R\right)}$$
11		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
12	1 9 4 11	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
13	12 8	sseldi	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
14	9 10 3 11 5 6 7 13	psrvsca	$$⊢\phi \to X\underset{\dot{}}{\bullet }F=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$