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

Metamath Proof Explorer

Theorem mavmulfv

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

Ref Expression
Hypotheses mavmulval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mavmulval.m ⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
mavmulval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mavmulval.t ⊢ · = ( .r ‘ 𝑅 )
mavmulval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
mavmulval.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mavmulval.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
mavmulval.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
mavmulfv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
Assertion mavmulfv ( 𝜑 → ( ( 𝑋 × 𝑌 ) ‘ 𝐼 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mavmulval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mavmulval.m ⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
3 mavmulval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 mavmulval.t ⊢ · = ( .r ‘ 𝑅 )
5 mavmulval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
6 mavmulval.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
7 mavmulval.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
8 mavmulval.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
9 mavmulfv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
10 1 2 3 4 5 6 7 8 mavmulval ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σ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 ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) )