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

Metamath Proof Explorer

Theorem mamufv

Description: A cell in the multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Hypotheses mamufval.f ⊢ F = R maMul M N P
mamufval.b ⊢ B = Base R
mamufval.t ⊢ · ˙ = ⋅ R
mamufval.r ⊢ φ → R ∈ V
mamufval.m ⊢ φ → M ∈ Fin
mamufval.n ⊢ φ → N ∈ Fin
mamufval.p ⊢ φ → P ∈ Fin
mamuval.x ⊢ φ → X ∈ B M × N
mamuval.y ⊢ φ → Y ∈ B N × P
mamufv.i ⊢ φ → I ∈ M
mamufv.k ⊢ φ → K ∈ P
Assertion mamufv ⊢ φ → I X F Y K = ∑ R j ∈ N I X j · ˙ j Y K

Proof

Step Hyp Ref Expression
1 mamufval.f ⊢ F = R maMul M N P
2 mamufval.b ⊢ B = Base R
3 mamufval.t ⊢ · ˙ = ⋅ R
4 mamufval.r ⊢ φ → R ∈ V
5 mamufval.m ⊢ φ → M ∈ Fin
6 mamufval.n ⊢ φ → N ∈ Fin
7 mamufval.p ⊢ φ → P ∈ Fin
8 mamuval.x ⊢ φ → X ∈ B M × N
9 mamuval.y ⊢ φ → Y ∈ B N × P
10 mamufv.i ⊢ φ → I ∈ M
11 mamufv.k ⊢ φ → K ∈ P
12 1 2 3 4 5 6 7 8 9 mamuval ⊢ φ → X F Y = i ∈ M , k ∈ P ⟼ ∑ R j ∈ N i X j · ˙ j Y k
13 oveq1 ⊢ i = I → i X j = I X j
14 oveq2 ⊢ k = K → j Y k = j Y K
15 13 14 oveqan12d ⊢ i = I ∧ k = K → i X j · ˙ j Y k = I X j · ˙ j Y K
16 15 adantl ⊢ φ ∧ i = I ∧ k = K → i X j · ˙ j Y k = I X j · ˙ j Y K
17 16 mpteq2dv ⊢ φ ∧ i = I ∧ k = K → j ∈ N ⟼ i X j · ˙ j Y k = j ∈ N ⟼ I X j · ˙ j Y K
18 17 oveq2d ⊢ φ ∧ i = I ∧ k = K → ∑ R j ∈ N i X j · ˙ j Y k = ∑ R j ∈ N I X j · ˙ j Y K
19 ovexd ⊢ φ → ∑ R j ∈ N I X j · ˙ j Y K ∈ V
20 12 18 10 11 19 ovmpod ⊢ φ → I X F Y K = ∑ R j ∈ N I X j · ˙ j Y K