mvmulfv

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

	Ref	Expression
Hypotheses	mvmulfval.x	$⊢ \underset{˙}{\times} = R maVecMul ⟨M, N⟩$
	mvmulfval.b	$⊢ B = {Base}_{R}$
	mvmulfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mvmulfval.r	$⊢ φ \to R \in V$
	mvmulfval.m	$⊢ φ \to M \in Fin$
	mvmulfval.n	$⊢ φ \to N \in Fin$
	mvmulval.x	$⊢ φ \to X \in (B^{(M \times N)})$
	mvmulval.y	$⊢ φ \to Y \in (B^{N})$
	mvmulfv.i	$⊢ φ \to I \in M$
Assertion	mvmulfv	$⊢ φ \to (X \underset{˙}{\times} Y) (I) = \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} Y (j))$

Step	Hyp	Ref	Expression
1		mvmulfval.x	$⊢ \underset{˙}{\times} = R maVecMul ⟨M, N⟩$
2		mvmulfval.b	$⊢ B = {Base}_{R}$
3		mvmulfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		mvmulfval.r	$⊢ φ \to R \in V$
5		mvmulfval.m	$⊢ φ \to M \in Fin$
6		mvmulfval.n	$⊢ φ \to N \in Fin$
7		mvmulval.x	$⊢ φ \to X \in (B^{(M \times N)})$
8		mvmulval.y	$⊢ φ \to Y \in (B^{N})$
9		mvmulfv.i	$⊢ φ \to I \in M$
10	1 2 3 4 5 6 7 8	mvmulval	$⊢ φ \to X \underset{˙}{\times} Y = (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$
11		oveq1	$⊢ i = I \to i X j = I X j$
12	11	adantl	$⊢ (φ \land i = I) \to i X j = I X j$
13	12	oveq1d	$⊢ (φ \land i = I) \to (i X j) \underset{˙}{\cdot} Y (j) = (I X j) \underset{˙}{\cdot} Y (j)$
14	13	mpteq2dv	$⊢ (φ \land i = I) \to (j \in N ⟼ (i X j) \underset{˙}{\cdot} Y (j)) = (j \in N ⟼ (I X j) \underset{˙}{\cdot} Y (j))$
15	14	oveq2d	$⊢ (φ \land i = I) \to \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)) = \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} Y (j))$
16		ovexd	$⊢ φ \to \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} Y (j)) \in V$
17	10 15 9 16	fvmptd	$⊢ φ \to (X \underset{˙}{\times} Y) (I) = \underset{j \in N}{\sum_{R}} ((I X j) \underset{˙}{\cdot} Y (j))$

Metamath Proof Explorer