Metamath Proof Explorer

Theorem mvmulval

Description: 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})$
	Assertion	mvmulval	$⊢ φ \to X \underset{˙}{\times} Y = (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$

Proof

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	1 2 3 4 5 6	mvmulfval	$⊢ φ \to \underset{˙}{\times} = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))))$
10		oveq	$⊢ x = X \to i x j = i X j$
11		fveq1	$⊢ y = Y \to y (j) = Y (j)$
12	10 11	oveqan12d	$⊢ (x = X \land y = Y) \to (i x j) \underset{˙}{\cdot} y (j) = (i X j) \underset{˙}{\cdot} Y (j)$
13	12	adantl	$⊢ (φ \land (x = X \land y = Y)) \to (i x j) \underset{˙}{\cdot} y (j) = (i X j) \underset{˙}{\cdot} Y (j)$
14	13	mpteq2dv	$⊢ (φ \land (x = X \land y = Y)) \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 (x = X \land y = Y)) \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	15	mpteq2dv	$⊢ (φ \land (x = X \land y = Y)) \to (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))) = (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$
17	5	mptexd	$⊢ φ \to (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j))) \in V$
18	9 16 7 8 17	ovmpod	$⊢ φ \to X \underset{˙}{\times} Y = (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$