mavmulval

Description: Multiplication of a vector with a square matrix. (Contributed 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})$
Assertion	mavmulval	$⊢ φ \to X \underset{˙}{\times} Y = (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$

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	1 3	matbas2	$⊢ (N \in Fin \land R \in V) \to B^{(N \times N)} = {Base}_{A}$
10	6 5 9	syl2anc	$⊢ φ \to B^{(N \times N)} = {Base}_{A}$
11	7 10	eleqtrrd	$⊢ φ \to X \in (B^{(N \times N)})$
12	2 3 4 5 6 6 11 8	mvmulval	$⊢ φ \to X \underset{˙}{\times} Y = (i \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \underset{˙}{\cdot} Y (j)))$

Metamath Proof Explorer