Metamath Proof Explorer

Theorem mavmulfv

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

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

Proof

Step	Hyp	Ref	Expression
1		mavmulval.a	$⊢ A = N Mat R$
2		mavmulval.m	$⊢ \underset{˙}{\times} = R maVecMul ⟨N, N⟩$
3		mavmulval.b	$⊢ B = {Base}_{R}$
4		mavmulval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		mavmulval.r	$⊢ φ \to R \in V$
6		mavmulval.n	$⊢ φ \to N \in Fin$
7		mavmulval.x	$⊢ φ \to X \in {Base}_{A}$
8		mavmulval.y	$⊢ φ \to Y \in (B^{N})$
9		mavmulfv.i	$⊢ φ \to I \in N$
10	1 2 3 4 5 6 7 8	mavmulval	$⊢ φ \to X \underset{˙}{\times} Y = (i \in N ⟼ \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))$