mamuvs1

Description: Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	mamucl.b	$⊢ B = {Base}_{R}$
	mamucl.r	$⊢ φ \to R \in Ring$
	mamudi.f	$⊢ F = R maMul ⟨M, N, O⟩$
	mamudi.m	$⊢ φ \to M \in Fin$
	mamudi.n	$⊢ φ \to N \in Fin$
	mamudi.o	$⊢ φ \to O \in Fin$
	mamuvs1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mamuvs1.x	$⊢ φ \to X \in B$
	mamuvs1.y	$⊢ φ \to Y \in (B^{(M \times N)})$
	mamuvs1.z	$⊢ φ \to Z \in (B^{(N \times O)})$
Assertion	mamuvs1	$⊢ φ \to (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z = ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)$

Proof

Step	Hyp	Ref	Expression
1		mamucl.b	$⊢ B = {Base}_{R}$
2		mamucl.r	$⊢ φ \to R \in Ring$
3		mamudi.f	$⊢ F = R maMul ⟨M, N, O⟩$
4		mamudi.m	$⊢ φ \to M \in Fin$
5		mamudi.n	$⊢ φ \to N \in Fin$
6		mamudi.o	$⊢ φ \to O \in Fin$
7		mamuvs1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mamuvs1.x	$⊢ φ \to X \in B$
9		mamuvs1.y	$⊢ φ \to Y \in (B^{(M \times N)})$
10		mamuvs1.z	$⊢ φ \to Z \in (B^{(N \times O)})$
11		eqid	$⊢ 0_{R} = 0_{R}$
12	2	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to R \in Ring$
13	5	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to N \in Fin$
14	8	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to X \in B$
15	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to R \in Ring$
16		elmapi	$⊢ Y \in (B^{(M \times N)}) \to Y : M \times N ⟶ B$
17	9 16	syl	$⊢ φ \to Y : M \times N ⟶ B$
18	17	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Y : M \times N ⟶ B$
19		simplrl	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to i \in M$
20		simpr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to j \in N$
21	18 19 20	fovcdmd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to i Y j \in B$
22		elmapi	$⊢ Z \in (B^{(N \times O)}) \to Z : N \times O ⟶ B$
23	10 22	syl	$⊢ φ \to Z : N \times O ⟶ B$
24	23	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Z : N \times O ⟶ B$
25		simplrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to k \in O$
26	24 20 25	fovcdmd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to j Z k \in B$
27	1 7 15 21 26	ringcld	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i Y j) \underset{˙}{\cdot} (j Z k) \in B$
28		eqid	$⊢ (j \in N ⟼ (i Y j) \underset{˙}{\cdot} (j Z k)) = (j \in N ⟼ (i Y j) \underset{˙}{\cdot} (j Z k))$
29		ovexd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i Y j) \underset{˙}{\cdot} (j Z k) \in V$
30		fvexd	$⊢ (φ \land (i \in M \land k \in O)) \to 0_{R} \in V$
31	28 13 29 30	fsuppmptdm	$⊢ (φ \land (i \in M \land k \in O)) \to {finSupp}_{0_{R}} ((j \in N ⟼ (i Y j) \underset{˙}{\cdot} (j Z k)))$
32	1 11 7 12 13 14 27 31	gsummulc2	$⊢ (φ \land (i \in M \land k \in O)) \to \underset{j \in N}{\sum_{R}} (X \underset{˙}{\cdot} ((i Y j) \underset{˙}{\cdot} (j Z k))) = X \underset{˙}{\cdot} (\underset{j \in N}{\sum_{R}}, ((i Y j) \underset{˙}{\cdot} (j Z k)))$
33		df-ov	$⊢ i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j = (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) (⟨i, j⟩)$
34		simprl	$⊢ (φ \land (i \in M \land k \in O)) \to i \in M$
35		opelxpi	$⊢ (i \in M \land j \in N) \to ⟨i, j⟩ \in (M \times N)$
36	34 35	sylan	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to ⟨i, j⟩ \in (M \times N)$
37		xpfi	$⊢ (M \in Fin \land N \in Fin) \to M \times N \in Fin$
38	4 5 37	syl2anc	$⊢ φ \to M \times N \in Fin$
39	38	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to M \times N \in Fin$
40	8	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to X \in B$
41		ffn	$⊢ Y : M \times N ⟶ B \to Y Fn (M \times N)$
42	9 16 41	3syl	$⊢ φ \to Y Fn (M \times N)$
43	42	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Y Fn (M \times N)$
44		df-ov	$⊢ i Y j = Y (⟨i, j⟩)$
45	44	eqcomi	$⊢ Y (⟨i, j⟩) = i Y j$
46	45	a1i	$⊢ (((φ \land (i \in M \land k \in O)) \land j \in N) \land ⟨i, j⟩ \in (M \times N)) \to Y (⟨i, j⟩) = i Y j$
47	39 40 43 46	ofc1	$⊢ (((φ \land (i \in M \land k \in O)) \land j \in N) \land ⟨i, j⟩ \in (M \times N)) \to (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) (⟨i, j⟩) = X \underset{˙}{\cdot} (i Y j)$
48	36 47	mpdan	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) (⟨i, j⟩) = X \underset{˙}{\cdot} (i Y j)$
49	33 48	eqtrid	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j = X \underset{˙}{\cdot} (i Y j)$
50	49	oveq1d	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j) \underset{˙}{\cdot} (j Z k) = (X \underset{˙}{\cdot} (i Y j)) \underset{˙}{\cdot} (j Z k)$
51	1 7	ringass	$⊢ (R \in Ring \land (X \in B \land i Y j \in B \land j Z k \in B)) \to (X \underset{˙}{\cdot} (i Y j)) \underset{˙}{\cdot} (j Z k) = X \underset{˙}{\cdot} ((i Y j) \underset{˙}{\cdot} (j Z k))$
52	15 40 21 26 51	syl13anc	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (X \underset{˙}{\cdot} (i Y j)) \underset{˙}{\cdot} (j Z k) = X \underset{˙}{\cdot} ((i Y j) \underset{˙}{\cdot} (j Z k))$
53	50 52	eqtrd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j) \underset{˙}{\cdot} (j Z k) = X \underset{˙}{\cdot} ((i Y j) \underset{˙}{\cdot} (j Z k))$
54	53	mpteq2dva	$⊢ (φ \land (i \in M \land k \in O)) \to (j \in N ⟼ (i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j) \underset{˙}{\cdot} (j Z k)) = (j \in N ⟼ X \underset{˙}{\cdot} ((i Y j) \underset{˙}{\cdot} (j Z k)))$
55	54	oveq2d	$⊢ (φ \land (i \in M \land k \in O)) \to \underset{j \in N}{\sum_{R}} ((i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j) \underset{˙}{\cdot} (j Z k)) = \underset{j \in N}{\sum_{R}} (X \underset{˙}{\cdot} ((i Y j) \underset{˙}{\cdot} (j Z k)))$
56	4	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \in Fin$
57	6	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to O \in Fin$
58	9	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Y \in (B^{(M \times N)})$
59	10	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Z \in (B^{(N \times O)})$
60		simprr	$⊢ (φ \land (i \in M \land k \in O)) \to k \in O$
61	3 1 7 12 56 13 57 58 59 34 60	mamufv	$⊢ (φ \land (i \in M \land k \in O)) \to i (Y F Z) k = \underset{j \in N}{\sum_{R}} ((i Y j) \underset{˙}{\cdot} (j Z k))$
62	61	oveq2d	$⊢ (φ \land (i \in M \land k \in O)) \to X \underset{˙}{\cdot} (i (Y F Z) k) = X \underset{˙}{\cdot} (\underset{j \in N}{\sum_{R}}, ((i Y j) \underset{˙}{\cdot} (j Z k)))$
63	32 55 62	3eqtr4d	$⊢ (φ \land (i \in M \land k \in O)) \to \underset{j \in N}{\sum_{R}} ((i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j) \underset{˙}{\cdot} (j Z k)) = X \underset{˙}{\cdot} (i (Y F Z) k)$
64		fconst6g	$⊢ X \in B \to ((M \times N) \times \{X\}) : M \times N ⟶ B$
65	8 64	syl	$⊢ φ \to ((M \times N) \times \{X\}) : M \times N ⟶ B$
66	1	fvexi	$⊢ B \in V$
67		elmapg	$⊢ (B \in V \land M \times N \in Fin) \to ((M \times N) \times \{X\} \in (B^{(M \times N)}) \leftrightarrow ((M \times N) \times \{X\}) : M \times N ⟶ B)$
68	66 38 67	sylancr	$⊢ φ \to ((M \times N) \times \{X\} \in (B^{(M \times N)}) \leftrightarrow ((M \times N) \times \{X\}) : M \times N ⟶ B)$
69	65 68	mpbird	$⊢ φ \to (M \times N) \times \{X\} \in (B^{(M \times N)})$
70	1 7	ringvcl	$⊢ (R \in Ring \land (M \times N) \times \{X\} \in (B^{(M \times N)}) \land Y \in (B^{(M \times N)})) \to ((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y \in (B^{(M \times N)})$
71	2 69 9 70	syl3anc	$⊢ φ \to ((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y \in (B^{(M \times N)})$
72	71	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to ((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y \in (B^{(M \times N)})$
73	3 1 7 12 56 13 57 72 59 34 60	mamufv	$⊢ (φ \land (i \in M \land k \in O)) \to i ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) k = \underset{j \in N}{\sum_{R}} ((i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j) \underset{˙}{\cdot} (j Z k))$
74		df-ov	$⊢ i (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) k = (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) (⟨i, k⟩)$
75		opelxpi	$⊢ (i \in M \land k \in O) \to ⟨i, k⟩ \in (M \times O)$
76	75	adantl	$⊢ (φ \land (i \in M \land k \in O)) \to ⟨i, k⟩ \in (M \times O)$
77		xpfi	$⊢ (M \in Fin \land O \in Fin) \to M \times O \in Fin$
78	4 6 77	syl2anc	$⊢ φ \to M \times O \in Fin$
79	78	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \times O \in Fin$
80	1 2 3 4 5 6 9 10	mamucl	$⊢ φ \to Y F Z \in (B^{(M \times O)})$
81		elmapi	$⊢ Y F Z \in (B^{(M \times O)}) \to (Y F Z) : M \times O ⟶ B$
82		ffn	$⊢ (Y F Z) : M \times O ⟶ B \to (Y F Z) Fn (M \times O)$
83	80 81 82	3syl	$⊢ φ \to (Y F Z) Fn (M \times O)$
84	83	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to (Y F Z) Fn (M \times O)$
85		df-ov	$⊢ i (Y F Z) k = (Y F Z) (⟨i, k⟩)$
86	85	eqcomi	$⊢ (Y F Z) (⟨i, k⟩) = i (Y F Z) k$
87	86	a1i	$⊢ ((φ \land (i \in M \land k \in O)) \land ⟨i, k⟩ \in (M \times O)) \to (Y F Z) (⟨i, k⟩) = i (Y F Z) k$
88	79 14 84 87	ofc1	$⊢ ((φ \land (i \in M \land k \in O)) \land ⟨i, k⟩ \in (M \times O)) \to (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) (⟨i, k⟩) = X \underset{˙}{\cdot} (i (Y F Z) k)$
89	76 88	mpdan	$⊢ (φ \land (i \in M \land k \in O)) \to (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) (⟨i, k⟩) = X \underset{˙}{\cdot} (i (Y F Z) k)$
90	74 89	eqtrid	$⊢ (φ \land (i \in M \land k \in O)) \to i (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) k = X \underset{˙}{\cdot} (i (Y F Z) k)$
91	63 73 90	3eqtr4d	$⊢ (φ \land (i \in M \land k \in O)) \to i ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) k = i (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) k$
92	91	ralrimivva	$⊢ φ \to \forall i \in M \forall k \in O i ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) k = i (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) k$
93	1 2 3 4 5 6 71 10	mamucl	$⊢ φ \to (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z \in (B^{(M \times O)})$
94		elmapi	$⊢ (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z \in (B^{(M \times O)}) \to ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) : M \times O ⟶ B$
95		ffn	$⊢ ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) : M \times O ⟶ B \to ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) Fn (M \times O)$
96	93 94 95	3syl	$⊢ φ \to ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) Fn (M \times O)$
97		fconst6g	$⊢ X \in B \to ((M \times O) \times \{X\}) : M \times O ⟶ B$
98	8 97	syl	$⊢ φ \to ((M \times O) \times \{X\}) : M \times O ⟶ B$
99		elmapg	$⊢ (B \in V \land M \times O \in Fin) \to ((M \times O) \times \{X\} \in (B^{(M \times O)}) \leftrightarrow ((M \times O) \times \{X\}) : M \times O ⟶ B)$
100	66 78 99	sylancr	$⊢ φ \to ((M \times O) \times \{X\} \in (B^{(M \times O)}) \leftrightarrow ((M \times O) \times \{X\}) : M \times O ⟶ B)$
101	98 100	mpbird	$⊢ φ \to (M \times O) \times \{X\} \in (B^{(M \times O)})$
102	1 7	ringvcl	$⊢ (R \in Ring \land (M \times O) \times \{X\} \in (B^{(M \times O)}) \land Y F Z \in (B^{(M \times O)})) \to ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z) \in (B^{(M \times O)})$
103	2 101 80 102	syl3anc	$⊢ φ \to ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z) \in (B^{(M \times O)})$
104		elmapi	$⊢ ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z) \in (B^{(M \times O)}) \to (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) : M \times O ⟶ B$
105		ffn	$⊢ (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) : M \times O ⟶ B \to (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) Fn (M \times O)$
106	103 104 105	3syl	$⊢ φ \to (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) Fn (M \times O)$
107		eqfnov2	$⊢ (((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) Fn (M \times O) \land (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) Fn (M \times O)) \to ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z = ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z) \leftrightarrow \forall i \in M \forall k \in O i ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) k = i (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) k)$
108	96 106 107	syl2anc	$⊢ φ \to ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z = ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z) \leftrightarrow \forall i \in M \forall k \in O i ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) k = i (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) k)$
109	92 108	mpbird	$⊢ φ \to (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z = ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)$

Metamath Proof Explorer

Theorem mamuvs1

Proof