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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mamufval.r	$⊢ φ \to R \in V$
	mamufval.m	$⊢ φ \to M \in Fin$
	mamufval.n	$⊢ φ \to N \in Fin$
	mamufval.p	$⊢ φ \to P \in Fin$
	mamuval.x	$⊢ φ \to X \in (B^{(M \times N)})$
	mamuval.y	$⊢ φ \to Y \in (B^{(N \times P)})$
	mamufv.i	$⊢ φ \to I \in M$
	mamufv.k	$⊢ φ \to K \in P$
Assertion	mamufv	$⊢ φ \to I (X F Y) K = \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} (j Y K))$

Step	Hyp	Ref	Expression
1		mamufval.f	$⊢ F = R maMul ⟨M, N, P⟩$
2		mamufval.b	$⊢ B = {Base}_{R}$
3		mamufval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		mamufval.r	$⊢ φ \to R \in V$
5		mamufval.m	$⊢ φ \to M \in Fin$
6		mamufval.n	$⊢ φ \to N \in Fin$
7		mamufval.p	$⊢ φ \to P \in Fin$
8		mamuval.x	$⊢ φ \to X \in (B^{(M \times N)})$
9		mamuval.y	$⊢ φ \to Y \in (B^{(N \times P)})$
10		mamufv.i	$⊢ φ \to I \in M$
11		mamufv.k	$⊢ φ \to K \in P$
12	1 2 3 4 5 6 7 8 9	mamuval	$⊢ φ \to X F Y = (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} (j Y k)))$
13		oveq1	$⊢ i = I \to i X j = I X j$
14		oveq2	$⊢ k = K \to j Y k = j Y K$
15	13 14	oveqan12d	$⊢ (i = I \land k = K) \to (i X j) \underset{˙}{\cdot} (j Y k) = (I X j) \underset{˙}{\cdot} (j Y K)$
16	15	adantl	$⊢ (φ \land (i = I \land k = K)) \to (i X j) \underset{˙}{\cdot} (j Y k) = (I X j) \underset{˙}{\cdot} (j Y K)$
17	16	mpteq2dv	$⊢ (φ \land (i = I \land k = K)) \to (j \in N ⟼ (i X j) \underset{˙}{\cdot} (j Y k)) = (j \in N ⟼ (I X j) \underset{˙}{\cdot} (j Y K))$
18	17	oveq2d	$⊢ (φ \land (i = I \land k = K)) \to \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} (j Y k)) = \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} (j Y K))$
19		ovexd	$⊢ φ \to \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} (j Y K)) \in V$
20	12 18 10 11 19	ovmpod	$⊢ φ \to I (X F Y) K = \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} (j Y K))$

Metamath Proof Explorer