Theorem mavmulval

Description: Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019)

	Ref	Expression
Hypotheses	mavmulval.a	$$⊢A=N\mathrm{Mat}R$$
	mavmulval.m	$$⊢\underset{\dot{}}{\times }=R\mathrm{maVecMul}⟨N,N⟩$$
	mavmulval.b	$$⊢B={\mathrm{Base}}_R$$
	mavmulval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mavmulval.r	$$⊢\phi \to R\in V$$
	mavmulval.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	mavmulval.x	$$⊢\phi \to X\in {\mathrm{Base}}_A$$
	mavmulval.y	$$⊢\phi \to Y\in \left(B^N\right)$$
Assertion	mavmulval	$$⊢\phi \to X\underset{\dot{}}{\times }Y=\left(i\in N⟼\underset{j\in N}{{\sum }_R}\left(\left(iXj\right)\underset{\dot{}}{·}Y\left(j\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mavmulval.a	$$⊢A=N\mathrm{Mat}R$$
2		mavmulval.m	$$⊢\underset{\dot{}}{\times }=R\mathrm{maVecMul}⟨N,N⟩$$
3		mavmulval.b	$$⊢B={\mathrm{Base}}_R$$
4		mavmulval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		mavmulval.r	$$⊢\phi \to R\in V$$
6		mavmulval.n	$$⊢\phi \to N\in \mathrm{Fin}$$
7		mavmulval.x	$$⊢\phi \to X\in {\mathrm{Base}}_A$$
8		mavmulval.y	$$⊢\phi \to Y\in \left(B^N\right)$$
9	1 3	matbas2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to B^{\left(N\times N\right)}={\mathrm{Base}}_A$$
10	6 5 9	syl2anc	$$⊢\phi \to B^{\left(N\times N\right)}={\mathrm{Base}}_A$$
11	7 10	eleqtrrd	$$⊢\phi \to X\in \left(B^{\left(N\times N\right)}\right)$$
12	2 3 4 5 6 6 11 8	mvmulval	$$⊢\phi \to X\underset{\dot{}}{\times }Y=\left(i\in N⟼\underset{j\in N}{{\sum }_R}\left(\left(iXj\right)\underset{\dot{}}{·}Y\left(j\right)\right)\right)$$