Theorem mplmul

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

	Ref	Expression
Hypotheses	mplmul.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mplmul.m	⊢ · = ( .r ‘ 𝑅 )
	mplmul.t	⊢ ∙ = ( .r ‘ 𝑃 )
	mplmul.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	mplmul.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	mplmul.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	mplmul	⊢ ( 𝜑 → ( 𝐹 ∙ 𝐺 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplmul.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		mplmul.m	⊢ · = ( .r ‘ 𝑅 )
4		mplmul.t	⊢ ∙ = ( .r ‘ 𝑃 )
5		mplmul.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
6		mplmul.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		mplmul.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
9		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
10	1 8 4	mplmulr	⊢ ∙ = ( .r ‘ ( 𝐼 mPwSer 𝑅 ) )
11	1 8 2 9	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
12	11 6	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
13	11 7	sselid	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
14	8 9 3 10 5 12 13	psrmulfval	⊢ ( 𝜑 → ( 𝐹 ∙ 𝐺 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )