Metamath Proof Explorer


Theorem mvmulfv

Description: A cell/element in the vector resulting from a multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019)

Ref Expression
Hypotheses mvmulfval.x × = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
mvmulfval.b 𝐵 = ( Base ‘ 𝑅 )
mvmulfval.t · = ( .r𝑅 )
mvmulfval.r ( 𝜑𝑅𝑉 )
mvmulfval.m ( 𝜑𝑀 ∈ Fin )
mvmulfval.n ( 𝜑𝑁 ∈ Fin )
mvmulval.x ( 𝜑𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
mvmulval.y ( 𝜑𝑌 ∈ ( 𝐵m 𝑁 ) )
mvmulfv.i ( 𝜑𝐼𝑀 )
Assertion mvmulfv ( 𝜑 → ( ( 𝑋 × 𝑌 ) ‘ 𝐼 ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mvmulfval.x × = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
2 mvmulfval.b 𝐵 = ( Base ‘ 𝑅 )
3 mvmulfval.t · = ( .r𝑅 )
4 mvmulfval.r ( 𝜑𝑅𝑉 )
5 mvmulfval.m ( 𝜑𝑀 ∈ Fin )
6 mvmulfval.n ( 𝜑𝑁 ∈ Fin )
7 mvmulval.x ( 𝜑𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
8 mvmulval.y ( 𝜑𝑌 ∈ ( 𝐵m 𝑁 ) )
9 mvmulfv.i ( 𝜑𝐼𝑀 )
10 1 2 3 4 5 6 7 8 mvmulval ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑖𝑀 ↦ ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) ) ) )
11 oveq1 ( 𝑖 = 𝐼 → ( 𝑖 𝑋 𝑗 ) = ( 𝐼 𝑋 𝑗 ) )
12 11 adantl ( ( 𝜑𝑖 = 𝐼 ) → ( 𝑖 𝑋 𝑗 ) = ( 𝐼 𝑋 𝑗 ) )
13 12 oveq1d ( ( 𝜑𝑖 = 𝐼 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) = ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) )
14 13 mpteq2dv ( ( 𝜑𝑖 = 𝐼 ) → ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) = ( 𝑗𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) )
15 14 oveq2d ( ( 𝜑𝑖 = 𝐼 ) → ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) ) )
16 ovexd ( 𝜑 → ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) ) ∈ V )
17 10 15 9 16 fvmptd ( 𝜑 → ( ( 𝑋 × 𝑌 ) ‘ 𝐼 ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌𝑗 ) ) ) ) )