mplmul

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

	Ref	Expression
Hypotheses	mplmul.p	$⊢ P = I mPoly R$
	mplmul.b	$⊢ B = {Base}_{P}$
	mplmul.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mplmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	mplmul.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	mplmul.f	$⊢ φ \to F \in B$
	mplmul.g	$⊢ φ \to G \in B$
Assertion	mplmul	$⊢ φ \to F \underset{˙}{∙} G = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (k -_{f} x)))$

Step	Hyp	Ref	Expression
1		mplmul.p	$⊢ P = I mPoly R$
2		mplmul.b	$⊢ B = {Base}_{P}$
3		mplmul.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		mplmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
5		mplmul.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
6		mplmul.f	$⊢ φ \to F \in B$
7		mplmul.g	$⊢ φ \to G \in B$
8		eqid	$⊢ I mPwSer R = I mPwSer R$
9		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
10	1 8 4	mplmulr	$⊢ \underset{˙}{∙} = \cdot_{(I mPwSer R)}$
11	1 8 2 9	mplbasss	$⊢ B \subseteq {Base}_{(I mPwSer R)}$
12	11 6	sselid	$⊢ φ \to F \in {Base}_{(I mPwSer R)}$
13	11 7	sselid	$⊢ φ \to G \in {Base}_{(I mPwSer R)}$
14	8 9 3 10 5 12 13	psrmulfval	$⊢ φ \to F \underset{˙}{∙} G = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (k -_{f} x)))$

Metamath Proof Explorer