Metamath Proof Explorer

Theorem mamuval

Description: 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
Assertion mamuval ⊢ φ → X F Y = i ∈ M , k ∈ P ⟼ ∑ 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 1 2 3 4 5 6 7 mamufval ⊢ φ → F = x ∈ B M × N , y ∈ B N × P ⟼ i ∈ M , k ∈ P ⟼ ∑ R j ∈ N i x j · ˙ j y k
11 oveq ⊢ x = X → i x j = i X j
12 oveq ⊢ y = Y → j y k = j Y k
13 11 12 oveqan12d ⊢ x = X ∧ y = Y → i x j · ˙ j y k = i X j · ˙ j Y k
14 13 adantl ⊢ φ ∧ x = X ∧ y = Y → i x j · ˙ j y k = i X j · ˙ j Y k
15 14 mpteq2dv ⊢ φ ∧ x = X ∧ y = Y → j ∈ N ⟼ i x j · ˙ j y k = j ∈ N ⟼ i X j · ˙ j Y k
16 15 oveq2d ⊢ φ ∧ x = X ∧ y = Y → ∑ R j ∈ N i x j · ˙ j y k = ∑ R j ∈ N i X j · ˙ j Y k
17 16 mpoeq3dv ⊢ φ ∧ x = X ∧ y = Y → i ∈ M , k ∈ P ⟼ ∑ R j ∈ N i x j · ˙ j y k = i ∈ M , k ∈ P ⟼ ∑ R j ∈ N i X j · ˙ j Y k
18 mpoexga ⊢ M ∈ Fin ∧ P ∈ Fin → i ∈ M , k ∈ P ⟼ ∑ R j ∈ N i X j · ˙ j Y k ∈ V
19 5 7 18 syl2anc ⊢ φ → i ∈ M , k ∈ P ⟼ ∑ R j ∈ N i X j · ˙ j Y k ∈ V
20 10 17 8 9 19 ovmpod ⊢ φ → X F Y = i ∈ M , k ∈ P ⟼ ∑ R j ∈ N i X j · ˙ j Y k