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 ⊢ A = N Mat R
mavmulval.m ⊢ × ˙ = R maVecMul N N
mavmulval.b ⊢ B = Base R
mavmulval.t ⊢ · ˙ = ⋅ R
mavmulval.r ⊢ φ → R ∈ V
mavmulval.n ⊢ φ → N ∈ Fin
mavmulval.x ⊢ φ → X ∈ Base A
mavmulval.y ⊢ φ → Y ∈ B N
mavmulfv.i ⊢ φ → I ∈ N
Assertion mavmulfv ⊢ φ → X × ˙ Y ⁡ I = ∑ R j ∈ N I X j · ˙ Y ⁡ j

Proof

Step Hyp Ref Expression
1 mavmulval.a ⊢ A = N Mat R
2 mavmulval.m ⊢ × ˙ = R maVecMul N N
3 mavmulval.b ⊢ B = Base R
4 mavmulval.t ⊢ · ˙ = ⋅ R
5 mavmulval.r ⊢ φ → R ∈ V
6 mavmulval.n ⊢ φ → N ∈ Fin
7 mavmulval.x ⊢ φ → X ∈ Base A
8 mavmulval.y ⊢ φ → Y ∈ B N
9 mavmulfv.i ⊢ φ → I ∈ N
10 1 2 3 4 5 6 7 8 mavmulval ⊢ φ → X × ˙ Y = i ∈ N ⟼ ∑ R j ∈ N i X j · ˙ Y ⁡ j
11 oveq1 ⊢ i = I → i X j = I X j
12 11 adantl ⊢ φ ∧ i = I → i X j = I X j
13 12 oveq1d ⊢ φ ∧ i = I → i X j · ˙ Y ⁡ j = I X j · ˙ Y ⁡ j
14 13 mpteq2dv ⊢ φ ∧ i = I → j ∈ N ⟼ i X j · ˙ Y ⁡ j = j ∈ N ⟼ I X j · ˙ Y ⁡ j
15 14 oveq2d ⊢ φ ∧ i = I → ∑ R j ∈ N i X j · ˙ Y ⁡ j = ∑ R j ∈ N I X j · ˙ Y ⁡ j
16 ovexd ⊢ φ → ∑ R j ∈ N I X j · ˙ Y ⁡ j ∈ V
17 10 15 9 16 fvmptd ⊢ φ → X × ˙ Y ⁡ I = ∑ R j ∈ N I X j · ˙ Y ⁡ j