mvmumamul1

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

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

Proof

Step	Hyp	Ref	Expression
1		mvmumamul1.x	$⊢ \underset{˙}{\times} = R maMul ⟨M, N, \{\emptyset\}⟩$
2		mvmumamul1.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨M, N⟩$
3		mvmumamul1.b	$⊢ B = {Base}_{R}$
4		mvmumamul1.r	$⊢ φ \to R \in Ring$
5		mvmumamul1.m	$⊢ φ \to M \in Fin$
6		mvmumamul1.n	$⊢ φ \to N \in Fin$
7		mvmumamul1.a	$⊢ φ \to A \in (B^{(M \times N)})$
8		mvmumamul1.y	$⊢ φ \to Y \in (B^{N})$
9		mvmumamul1.z	$⊢ φ \to Z \in (B^{(N \times \{\emptyset\})})$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	4	adantr	$⊢ (φ \land i \in M) \to R \in Ring$
12	5	adantr	$⊢ (φ \land i \in M) \to M \in Fin$
13	6	adantr	$⊢ (φ \land i \in M) \to N \in Fin$
14	7	adantr	$⊢ (φ \land i \in M) \to A \in (B^{(M \times N)})$
15	8	adantr	$⊢ (φ \land i \in M) \to Y \in (B^{N})$
16		simpr	$⊢ (φ \land i \in M) \to i \in M$
17	2 3 10 11 12 13 14 15 16	mvmulfv	$⊢ (φ \land i \in M) \to (A \underset{˙}{\cdot} Y) (i) = \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} Y (k))$
18	17	adantlr	$⊢ ((φ \land \forall j \in N Y (j) = j Z \emptyset) \land i \in M) \to (A \underset{˙}{\cdot} Y) (i) = \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} Y (k))$
19		fveq2	$⊢ j = k \to Y (j) = Y (k)$
20		oveq1	$⊢ j = k \to j Z \emptyset = k Z \emptyset$
21	19 20	eqeq12d	$⊢ j = k \to (Y (j) = j Z \emptyset \leftrightarrow Y (k) = k Z \emptyset)$
22	21	rspccv	$⊢ \forall j \in N Y (j) = j Z \emptyset \to (k \in N \to Y (k) = k Z \emptyset)$
23	22	adantl	$⊢ (φ \land \forall j \in N Y (j) = j Z \emptyset) \to (k \in N \to Y (k) = k Z \emptyset)$
24	23	imp	$⊢ ((φ \land \forall j \in N Y (j) = j Z \emptyset) \land k \in N) \to Y (k) = k Z \emptyset$
25	24	oveq2d	$⊢ ((φ \land \forall j \in N Y (j) = j Z \emptyset) \land k \in N) \to (i A k) \cdot_{R} Y (k) = (i A k) \cdot_{R} (k Z \emptyset)$
26	25	mpteq2dva	$⊢ (φ \land \forall j \in N Y (j) = j Z \emptyset) \to (k \in N ⟼ (i A k) \cdot_{R} Y (k)) = (k \in N ⟼ (i A k) \cdot_{R} (k Z \emptyset))$
27	26	oveq2d	$⊢ (φ \land \forall j \in N Y (j) = j Z \emptyset) \to \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} Y (k)) = \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} (k Z \emptyset))$
28	27	adantr	$⊢ ((φ \land \forall j \in N Y (j) = j Z \emptyset) \land i \in M) \to \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} Y (k)) = \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} (k Z \emptyset))$
29		snfi	$⊢ \{\emptyset\} \in Fin$
30	29	a1i	$⊢ (φ \land i \in M) \to \{\emptyset\} \in Fin$
31	9	adantr	$⊢ (φ \land i \in M) \to Z \in (B^{(N \times \{\emptyset\})})$
32		0ex	$⊢ \emptyset \in V$
33	32	snid	$⊢ \emptyset \in \{\emptyset\}$
34	33	a1i	$⊢ (φ \land i \in M) \to \emptyset \in \{\emptyset\}$
35	1 3 10 11 12 13 30 14 31 16 34	mamufv	$⊢ (φ \land i \in M) \to i (A \underset{˙}{\times} Z) \emptyset = \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} (k Z \emptyset))$
36	35	eqcomd	$⊢ (φ \land i \in M) \to \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} (k Z \emptyset)) = i (A \underset{˙}{\times} Z) \emptyset$
37	36	adantlr	$⊢ ((φ \land \forall j \in N Y (j) = j Z \emptyset) \land i \in M) \to \underset{k \in N}{\sum_{R}} ((i A k) \cdot_{R} (k Z \emptyset)) = i (A \underset{˙}{\times} Z) \emptyset$
38	18 28 37	3eqtrd	$⊢ ((φ \land \forall j \in N Y (j) = j Z \emptyset) \land i \in M) \to (A \underset{˙}{\cdot} Y) (i) = i (A \underset{˙}{\times} Z) \emptyset$
39	38	ralrimiva	$⊢ (φ \land \forall j \in N Y (j) = j Z \emptyset) \to \forall i \in M (A \underset{˙}{\cdot} Y) (i) = i (A \underset{˙}{\times} Z) \emptyset$
40	39	ex	$⊢ φ \to (\forall j \in N Y (j) = j Z \emptyset \to \forall i \in M (A \underset{˙}{\cdot} Y) (i) = i (A \underset{˙}{\times} Z) \emptyset)$

Metamath Proof Explorer

Theorem mvmumamul1

Proof