Theorem mplmul

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

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

Proof

Step	Hyp	Ref	Expression
1		mplmul.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplmul.b	$$⊢B={\mathrm{Base}}_P$$
3		mplmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		mplmul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
5		mplmul.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		mplmul.f	$$⊢\phi \to F\in B$$
7		mplmul.g	$$⊢\phi \to G\in B$$
8		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
9		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
10	1 8 4	mplmulr	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(I\mathrm{mPwSer}R\right)}$$
11	1 8 2 9	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
12	11 6	sselid	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
13	11 7	sselid	$$⊢\phi \to G\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
14	8 9 3 10 5 12 13	psrmulfval	$$⊢\phi \to F\underset{\dot{}}{\bullet }G=\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)\right)$$