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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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𝑥 ) ) ) ) ) ) )