Metamath Proof Explorer

Theorem mavmumamul1

Description: The multiplication of an NxN matrix with an N-dimensional vector corresponds to the matrix multiplication of an NxN matrix with an Nx1 matrix. (Contributed by AV, 14-Mar-2019)

		Ref	Expression
	Hypotheses	mavmumamul1.a	$⊢ A = N Mat R$
		mavmumamul1.m	$⊢ \underset{˙}{\times} = R maMul ⟨N, N, \{\emptyset\}⟩$
		mavmumamul1.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
		mavmumamul1.b	$⊢ B = {Base}_{R}$
		mavmumamul1.r	$⊢ φ \to R \in Ring$
		mavmumamul1.n	$⊢ φ \to N \in Fin$
		mavmumamul1.x	$⊢ φ \to X \in {Base}_{A}$
		mavmumamul1.y	$⊢ φ \to Y \in (B^{N})$
		mavmumamul1.z	$⊢ φ \to Z \in (B^{(N \times \{\emptyset\})})$
	Assertion	mavmumamul1	$⊢ φ \to (\forall j \in N Y (j) = j Z \emptyset \to \forall i \in N (X \underset{˙}{\cdot} Y) (i) = i (X \underset{˙}{\times} Z) \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		mavmumamul1.a	$⊢ A = N Mat R$
2		mavmumamul1.m	$⊢ \underset{˙}{\times} = R maMul ⟨N, N, \{\emptyset\}⟩$
3		mavmumamul1.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
4		mavmumamul1.b	$⊢ B = {Base}_{R}$
5		mavmumamul1.r	$⊢ φ \to R \in Ring$
6		mavmumamul1.n	$⊢ φ \to N \in Fin$
7		mavmumamul1.x	$⊢ φ \to X \in {Base}_{A}$
8		mavmumamul1.y	$⊢ φ \to Y \in (B^{N})$
9		mavmumamul1.z	$⊢ φ \to Z \in (B^{(N \times \{\emptyset\})})$
10	1 4	matbas2	$⊢ (N \in Fin \land R \in Ring) \to B^{(N \times N)} = {Base}_{A}$
11	6 5 10	syl2anc	$⊢ φ \to B^{(N \times N)} = {Base}_{A}$
12	7 11	eleqtrrd	$⊢ φ \to X \in (B^{(N \times N)})$
13	2 3 4 5 6 6 12 8 9	mvmumamul1	$⊢ φ \to (\forall j \in N Y (j) = j Z \emptyset \to \forall i \in N (X \underset{˙}{\cdot} Y) (i) = i (X \underset{˙}{\times} Z) \emptyset)$