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	2	fvexi	$$⊢B\in \mathrm{V}$$
11	1 8 2	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}B$$
12		eqid	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_{\left(I\mathrm{mPwSer}R\right)}$$
13	11 12	ressmulr	$$⊢B\in \mathrm{V}\to {\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_P$$
14	10 13	ax-mp	$$⊢{\cdot }_{\left(I\mathrm{mPwSer}R\right)}={\cdot }_P$$
15	4 14	eqtr4i	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\left(I\mathrm{mPwSer}R\right)}$$
16	1 8 2 9	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
17	16 6	sseldi	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
18	16 7	sseldi	$$⊢\phi \to G\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
19	8 9 3 15 5 17 18	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)$$