Theorem mplvscaval

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-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$$
	mplvscaval.y	$$⊢\phi \to Y\in D$$
Assertion	mplvscaval	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$

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		mplvscaval.y	$$⊢\phi \to Y\in D$$
10	1 2 3 4 5 6 7 8	mplvsca	$$⊢\phi \to X\underset{\dot{}}{\bullet }F=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$
11	10	fveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }F\right)\left(Y\right)=\left(\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F\right)\left(Y\right)$$
12		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
13	6 12	rabex2	$$⊢D\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to D\in \mathrm{V}$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16	1 15 4 6 8	mplelf	$$⊢\phi \to F:D⟶{\mathrm{Base}}_R$$
17	16	ffnd	$$⊢\phi \to FFnD$$
18		eqidd	$$⊢\left(\phi \wedge Y\in D\right)\to F\left(Y\right)=F\left(Y\right)$$
19	14 7 17 18	ofc1	$$⊢\left(\phi \wedge Y\in D\right)\to \left(\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$
20	9 19	mpdan	$$⊢\phi \to \left(\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$
21	11 20	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$