This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 − 𝑥 ) ) ) ) ) ) )