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	2	fvexi	⊢ 𝐵 ∈ V
11	1 8 2	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s 𝐵 )
12		eqid	⊢ ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ ( 𝐼 mPwSer 𝑅 ) )
13	11 12	ressmulr	⊢ ( 𝐵 ∈ V → ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ 𝑃 ) )
14	10 13	ax-mp	⊢ ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ 𝑃 )
15	4 14	eqtr4i	⊢ ∙ = ( .r ‘ ( 𝐼 mPwSer 𝑅 ) )
16	1 8 2 9	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
17	16 6	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
18	16 7	sselid	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
19	8 9 3 15 5 17 18	psrmulfval	⊢ ( 𝜑 → ( 𝐹 ∙ 𝐺 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )