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		eqid	$⊢ +_{R} = +_{R}$
13	2	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to R \in Ring$
14	5	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to N \in Fin$
15	8	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to X \in B$
16	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to R \in Ring$
17		elmapi	$⊢ Y \in (B^{(M \times N)}) \to Y : M \times N ⟶ B$
18	9 17	syl	$⊢ φ \to Y : M \times N ⟶ B$
19	18	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Y : M \times N ⟶ B$
20		simplrl	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to i \in M$
21		simpr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to j \in N$
22	19 20 21	fovrnd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to i Y j \in B$
23		elmapi	$⊢ Z \in (B^{(N \times O)}) \to Z : N \times O ⟶ B$
24	10 23	syl	$⊢ φ \to Z : N \times O ⟶ B$
25	24	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Z : N \times O ⟶ B$
26		simplrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to k \in O$
27	25 21 26	fovrnd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to j Z k \in B$
28	1 7	ringcl	$⊢ (R \in Ring \land i Y j \in B \land j Z k \in B) \to (i Y j) \underset{˙}{\cdot} (j Z k) \in B$
29	16 22 27 28	syl3anc	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i Y j) \underset{˙}{\cdot} (j Z k) \in B$
30		eqid	$⊢ (j \in N ⟼ (i Y j) \underset{˙}{\cdot} (j Z k)) = (j \in N ⟼ (i Y j) \underset{˙}{\cdot} (j Z k))$
31		ovexd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i Y j) \underset{˙}{\cdot} (j Z k) \in V$
32		fvexd	$⊢ (φ \land (i \in M \land k \in O)) \to 0_{R} \in V$
33	30 14 31 32	fsuppmptdm	$⊢ (φ \land (i \in M \land k \in O)) \to {finSupp}_{0_{R}} ((j \in N ⟼ (i Y j) \underset{˙}{\cdot} (j Z k)))$
34	1 11 12 7 13 14 15 29 33	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)))$
35		df-ov	$⊢ i (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) j = (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) (⟨i, j⟩)$
36		simprl	$⊢ (φ \land (i \in M \land k \in O)) \to i \in M$
37		opelxpi	$⊢ (i \in M \land j \in N) \to ⟨i, j⟩ \in (M \times N)$
38	36 37	sylan	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to ⟨i, j⟩ \in (M \times N)$
39		xpfi	$⊢ (M \in Fin \land N \in Fin) \to M \times N \in Fin$
40	4 5 39	syl2anc	$⊢ φ \to M \times N \in Fin$
41	40	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to M \times N \in Fin$
42	8	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to X \in B$
43		ffn	$⊢ Y : M \times N ⟶ B \to Y Fn (M \times N)$
44	9 17 43	3syl	$⊢ φ \to Y Fn (M \times N)$
45	44	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Y Fn (M \times N)$
46		df-ov	$⊢ i Y j = Y (⟨i, j⟩)$
47	46	eqcomi	$⊢ Y (⟨i, j⟩) = i Y j$
48	47	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$
49	41 42 45 48	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)$
50	38 49	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)$
51	35 50	syl5eq	$⊢ ((φ \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)$
52	51	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)$
53	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))$
54	16 42 22 27 53	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))$
55	52 54	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))$
56	55	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)))$
57	56	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)))$
58	4	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \in Fin$
59	6	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to O \in Fin$
60	9	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Y \in (B^{(M \times N)})$
61	10	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Z \in (B^{(N \times O)})$
62		simprr	$⊢ (φ \land (i \in M \land k \in O)) \to k \in O$
63	3 1 7 13 58 14 59 60 61 36 62	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))$
64	63	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)))$
65	34 57 64	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)$
66		fconst6g	$⊢ X \in B \to ((M \times N) \times \{X\}) : M \times N ⟶ B$
67	8 66	syl	$⊢ φ \to ((M \times N) \times \{X\}) : M \times N ⟶ B$
68	1	fvexi	$⊢ B \in V$
69		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)$
70	68 40 69	sylancr	$⊢ φ \to ((M \times N) \times \{X\} \in (B^{(M \times N)}) \leftrightarrow ((M \times N) \times \{X\}) : M \times N ⟶ B)$
71	67 70	mpbird	$⊢ φ \to (M \times N) \times \{X\} \in (B^{(M \times N)})$
72	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)})$
73	2 71 9 72	syl3anc	$⊢ φ \to ((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y \in (B^{(M \times N)})$
74	73	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to ((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y \in (B^{(M \times N)})$
75	3 1 7 13 58 14 59 74 61 36 62	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))$
76		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⟩)$
77		opelxpi	$⊢ (i \in M \land k \in O) \to ⟨i, k⟩ \in (M \times O)$
78	77	adantl	$⊢ (φ \land (i \in M \land k \in O)) \to ⟨i, k⟩ \in (M \times O)$
79		xpfi	$⊢ (M \in Fin \land O \in Fin) \to M \times O \in Fin$
80	4 6 79	syl2anc	$⊢ φ \to M \times O \in Fin$
81	80	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \times O \in Fin$
82	1 2 3 4 5 6 9 10	mamucl	$⊢ φ \to Y F Z \in (B^{(M \times O)})$
83		elmapi	$⊢ Y F Z \in (B^{(M \times O)}) \to (Y F Z) : M \times O ⟶ B$
84		ffn	$⊢ (Y F Z) : M \times O ⟶ B \to (Y F Z) Fn (M \times O)$
85	82 83 84	3syl	$⊢ φ \to (Y F Z) Fn (M \times O)$
86	85	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to (Y F Z) Fn (M \times O)$
87		df-ov	$⊢ i (Y F Z) k = (Y F Z) (⟨i, k⟩)$
88	87	eqcomi	$⊢ (Y F Z) (⟨i, k⟩) = i (Y F Z) k$
89	88	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$
90	81 15 86 89	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)$
91	78 90	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)$
92	76 91	syl5eq	$⊢ (φ \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)$
93	65 75 92	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$
94	93	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$
95	1 2 3 4 5 6 73 10	mamucl	$⊢ φ \to (((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z \in (B^{(M \times O)})$
96		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$
97		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)$
98	95 96 97	3syl	$⊢ φ \to ((((M \times N) \times \{X\}) {\underset{˙}{\cdot}}_{f} Y) F Z) Fn (M \times O)$
99		fconst6g	$⊢ X \in B \to ((M \times O) \times \{X\}) : M \times O ⟶ B$
100	8 99	syl	$⊢ φ \to ((M \times O) \times \{X\}) : M \times O ⟶ B$
101		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)$
102	68 80 101	sylancr	$⊢ φ \to ((M \times O) \times \{X\} \in (B^{(M \times O)}) \leftrightarrow ((M \times O) \times \{X\}) : M \times O ⟶ B)$
103	100 102	mpbird	$⊢ φ \to (M \times O) \times \{X\} \in (B^{(M \times O)})$
104	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)})$
105	2 103 82 104	syl3anc	$⊢ φ \to ((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z) \in (B^{(M \times O)})$
106		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$
107		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)$
108	105 106 107	3syl	$⊢ φ \to (((M \times O) \times \{X\}) {\underset{˙}{\cdot}}_{f} (Y F Z)) Fn (M \times O)$
109		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)$
110	98 108 109	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)$
111	94 110	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