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