mamudi

Description: Matrix multiplication distributes over addition on the left. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 23-Jul-2019)

	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$
	mamudi.p	$⊢ \underset{˙}{+} = +_{R}$
	mamudi.x	$⊢ φ \to X \in (B^{(M \times N)})$
	mamudi.y	$⊢ φ \to Y \in (B^{(M \times N)})$
	mamudi.z	$⊢ φ \to Z \in (B^{(N \times O)})$
Assertion	mamudi	$⊢ φ \to (X {\underset{˙}{+}}_{f} Y) F Z = (X F Z) {\underset{˙}{+}}_{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		mamudi.p	$⊢ \underset{˙}{+} = +_{R}$
8		mamudi.x	$⊢ φ \to X \in (B^{(M \times N)})$
9		mamudi.y	$⊢ φ \to Y \in (B^{(M \times N)})$
10		mamudi.z	$⊢ φ \to Z \in (B^{(N \times O)})$
11		ringcmn	$⊢ R \in Ring \to R \in CMnd$
12	2 11	syl	$⊢ φ \to R \in CMnd$
13	12	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to R \in CMnd$
14	5	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to N \in Fin$
15	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to R \in Ring$
16		elmapi	$⊢ X \in (B^{(M \times N)}) \to X : M \times N ⟶ B$
17	8 16	syl	$⊢ φ \to X : M \times N ⟶ B$
18	17	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to X : 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 X 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		eqid	$⊢ \cdot_{R} = \cdot_{R}$
28	1 27	ringcl	$⊢ (R \in Ring \land i X j \in B \land j Z k \in B) \to (i X j) \cdot_{R} (j Z k) \in B$
29	15 21 26 28	syl3anc	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i X j) \cdot_{R} (j Z k) \in B$
30		elmapi	$⊢ Y \in (B^{(M \times N)}) \to Y : M \times N ⟶ B$
31	9 30	syl	$⊢ φ \to Y : M \times N ⟶ B$
32	31	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Y : M \times N ⟶ B$
33	32 19 20	fovcdmd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to i Y j \in B$
34	1 27	ringcl	$⊢ (R \in Ring \land i Y j \in B \land j Z k \in B) \to (i Y j) \cdot_{R} (j Z k) \in B$
35	15 33 26 34	syl3anc	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i Y j) \cdot_{R} (j Z k) \in B$
36		eqid	$⊢ (j \in N ⟼ (i X j) \cdot_{R} (j Z k)) = (j \in N ⟼ (i X j) \cdot_{R} (j Z k))$
37		eqid	$⊢ (j \in N ⟼ (i Y j) \cdot_{R} (j Z k)) = (j \in N ⟼ (i Y j) \cdot_{R} (j Z k))$
38	1 7 13 14 29 35 36 37	gsummptfidmadd2	$⊢ (φ \land (i \in M \land k \in O)) \to \sum_{R} ((j \in N ⟼ (i X j) \cdot_{R} (j Z k)) {\underset{˙}{+}}_{f} (j \in N ⟼ (i Y j) \cdot_{R} (j Z k))) = (\underset{j \in N}{\sum_{R}}, ((i X j) \cdot_{R} (j Z k))) \underset{˙}{+} (\underset{j \in N}{\sum_{R}}, ((i Y j) \cdot_{R} (j Z k)))$
39	8	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to X \in (B^{(M \times N)})$
40		ffn	$⊢ X : M \times N ⟶ B \to X Fn (M \times N)$
41	39 16 40	3syl	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to X Fn (M \times N)$
42	9	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Y \in (B^{(M \times N)})$
43		ffn	$⊢ Y : M \times N ⟶ B \to Y Fn (M \times N)$
44	42 30 43	3syl	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to Y Fn (M \times N)$
45		xpfi	$⊢ (M \in Fin \land N \in Fin) \to M \times N \in Fin$
46	4 5 45	syl2anc	$⊢ φ \to M \times N \in Fin$
47	46	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to M \times N \in Fin$
48		opelxpi	$⊢ (i \in M \land j \in N) \to ⟨i, j⟩ \in (M \times N)$
49	48	adantlr	$⊢ ((i \in M \land k \in O) \land j \in N) \to ⟨i, j⟩ \in (M \times N)$
50	49	adantll	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to ⟨i, j⟩ \in (M \times N)$
51		fnfvof	$⊢ ((X Fn (M \times N) \land Y Fn (M \times N)) \land (M \times N \in Fin \land ⟨i, j⟩ \in (M \times N))) \to (X {\underset{˙}{+}}_{f} Y) (⟨i, j⟩) = X (⟨i, j⟩) \underset{˙}{+} Y (⟨i, j⟩)$
52	41 44 47 50 51	syl22anc	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (X {\underset{˙}{+}}_{f} Y) (⟨i, j⟩) = X (⟨i, j⟩) \underset{˙}{+} Y (⟨i, j⟩)$
53		df-ov	$⊢ i (X {\underset{˙}{+}}_{f} Y) j = (X {\underset{˙}{+}}_{f} Y) (⟨i, j⟩)$
54		df-ov	$⊢ i X j = X (⟨i, j⟩)$
55		df-ov	$⊢ i Y j = Y (⟨i, j⟩)$
56	54 55	oveq12i	$⊢ (i X j) \underset{˙}{+} (i Y j) = X (⟨i, j⟩) \underset{˙}{+} Y (⟨i, j⟩)$
57	52 53 56	3eqtr4g	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to i (X {\underset{˙}{+}}_{f} Y) j = (i X j) \underset{˙}{+} (i Y j)$
58	57	oveq1d	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i (X {\underset{˙}{+}}_{f} Y) j) \cdot_{R} (j Z k) = ((i X j) \underset{˙}{+} (i Y j)) \cdot_{R} (j Z k)$
59	1 7 27	ringdir	$⊢ (R \in Ring \land (i X j \in B \land i Y j \in B \land j Z k \in B)) \to ((i X j) \underset{˙}{+} (i Y j)) \cdot_{R} (j Z k) = ((i X j) \cdot_{R} (j Z k)) \underset{˙}{+} ((i Y j) \cdot_{R} (j Z k))$
60	15 21 33 26 59	syl13anc	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to ((i X j) \underset{˙}{+} (i Y j)) \cdot_{R} (j Z k) = ((i X j) \cdot_{R} (j Z k)) \underset{˙}{+} ((i Y j) \cdot_{R} (j Z k))$
61	58 60	eqtrd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i (X {\underset{˙}{+}}_{f} Y) j) \cdot_{R} (j Z k) = ((i X j) \cdot_{R} (j Z k)) \underset{˙}{+} ((i Y j) \cdot_{R} (j Z k))$
62	61	mpteq2dva	$⊢ (φ \land (i \in M \land k \in O)) \to (j \in N ⟼ (i (X {\underset{˙}{+}}_{f} Y) j) \cdot_{R} (j Z k)) = (j \in N ⟼ ((i X j) \cdot_{R} (j Z k)) \underset{˙}{+} ((i Y j) \cdot_{R} (j Z k)))$
63		eqidd	$⊢ (φ \land (i \in M \land k \in O)) \to (j \in N ⟼ (i X j) \cdot_{R} (j Z k)) = (j \in N ⟼ (i X j) \cdot_{R} (j Z k))$
64		eqidd	$⊢ (φ \land (i \in M \land k \in O)) \to (j \in N ⟼ (i Y j) \cdot_{R} (j Z k)) = (j \in N ⟼ (i Y j) \cdot_{R} (j Z k))$
65	14 29 35 63 64	offval2	$⊢ (φ \land (i \in M \land k \in O)) \to (j \in N ⟼ (i X j) \cdot_{R} (j Z k)) {\underset{˙}{+}}_{f} (j \in N ⟼ (i Y j) \cdot_{R} (j Z k)) = (j \in N ⟼ ((i X j) \cdot_{R} (j Z k)) \underset{˙}{+} ((i Y j) \cdot_{R} (j Z k)))$
66	62 65	eqtr4d	$⊢ (φ \land (i \in M \land k \in O)) \to (j \in N ⟼ (i (X {\underset{˙}{+}}_{f} Y) j) \cdot_{R} (j Z k)) = (j \in N ⟼ (i X j) \cdot_{R} (j Z k)) {\underset{˙}{+}}_{f} (j \in N ⟼ (i Y j) \cdot_{R} (j Z k))$
67	66	oveq2d	$⊢ (φ \land (i \in M \land k \in O)) \to \underset{j \in N}{\sum_{R}} ((i (X {\underset{˙}{+}}_{f} Y) j) \cdot_{R} (j Z k)) = \sum_{R} ((j \in N ⟼ (i X j) \cdot_{R} (j Z k)) {\underset{˙}{+}}_{f} (j \in N ⟼ (i Y j) \cdot_{R} (j Z k)))$
68	2	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to R \in Ring$
69	4	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \in Fin$
70	6	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to O \in Fin$
71	8	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to X \in (B^{(M \times N)})$
72	10	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Z \in (B^{(N \times O)})$
73		simprl	$⊢ (φ \land (i \in M \land k \in O)) \to i \in M$
74		simprr	$⊢ (φ \land (i \in M \land k \in O)) \to k \in O$
75	3 1 27 68 69 14 70 71 72 73 74	mamufv	$⊢ (φ \land (i \in M \land k \in O)) \to i (X F Z) k = \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Z k))$
76	9	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Y \in (B^{(M \times N)})$
77	3 1 27 68 69 14 70 76 72 73 74	mamufv	$⊢ (φ \land (i \in M \land k \in O)) \to i (Y F Z) k = \underset{j \in N}{\sum_{R}} ((i Y j) \cdot_{R} (j Z k))$
78	75 77	oveq12d	$⊢ (φ \land (i \in M \land k \in O)) \to (i (X F Z) k) \underset{˙}{+} (i (Y F Z) k) = (\underset{j \in N}{\sum_{R}}, ((i X j) \cdot_{R} (j Z k))) \underset{˙}{+} (\underset{j \in N}{\sum_{R}}, ((i Y j) \cdot_{R} (j Z k)))$
79	38 67 78	3eqtr4d	$⊢ (φ \land (i \in M \land k \in O)) \to \underset{j \in N}{\sum_{R}} ((i (X {\underset{˙}{+}}_{f} Y) j) \cdot_{R} (j Z k)) = (i (X F Z) k) \underset{˙}{+} (i (Y F Z) k)$
80		ringmnd	$⊢ R \in Ring \to R \in Mnd$
81	2 80	syl	$⊢ φ \to R \in Mnd$
82	1 7	mndvcl	$⊢ (R \in Mnd \land X \in (B^{(M \times N)}) \land Y \in (B^{(M \times N)})) \to X {\underset{˙}{+}}_{f} Y \in (B^{(M \times N)})$
83	81 8 9 82	syl3anc	$⊢ φ \to X {\underset{˙}{+}}_{f} Y \in (B^{(M \times N)})$
84	83	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to X {\underset{˙}{+}}_{f} Y \in (B^{(M \times N)})$
85	3 1 27 68 69 14 70 84 72 73 74	mamufv	$⊢ (φ \land (i \in M \land k \in O)) \to i ((X {\underset{˙}{+}}_{f} Y) F Z) k = \underset{j \in N}{\sum_{R}} ((i (X {\underset{˙}{+}}_{f} Y) j) \cdot_{R} (j Z k))$
86	1 2 3 4 5 6 8 10	mamucl	$⊢ φ \to X F Z \in (B^{(M \times O)})$
87		elmapi	$⊢ X F Z \in (B^{(M \times O)}) \to (X F Z) : M \times O ⟶ B$
88		ffn	$⊢ (X F Z) : M \times O ⟶ B \to (X F Z) Fn (M \times O)$
89	86 87 88	3syl	$⊢ φ \to (X F Z) Fn (M \times O)$
90	89	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to (X F Z) Fn (M \times O)$
91	1 2 3 4 5 6 9 10	mamucl	$⊢ φ \to Y F Z \in (B^{(M \times O)})$
92		elmapi	$⊢ Y F Z \in (B^{(M \times O)}) \to (Y F Z) : M \times O ⟶ B$
93		ffn	$⊢ (Y F Z) : M \times O ⟶ B \to (Y F Z) Fn (M \times O)$
94	91 92 93	3syl	$⊢ φ \to (Y F Z) Fn (M \times O)$
95	94	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to (Y F Z) Fn (M \times O)$
96		xpfi	$⊢ (M \in Fin \land O \in Fin) \to M \times O \in Fin$
97	4 6 96	syl2anc	$⊢ φ \to M \times O \in Fin$
98	97	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \times O \in Fin$
99		opelxpi	$⊢ (i \in M \land k \in O) \to ⟨i, k⟩ \in (M \times O)$
100	99	adantl	$⊢ (φ \land (i \in M \land k \in O)) \to ⟨i, k⟩ \in (M \times O)$
101		fnfvof	$⊢ (((X F Z) Fn (M \times O) \land (Y F Z) Fn (M \times O)) \land (M \times O \in Fin \land ⟨i, k⟩ \in (M \times O))) \to ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) (⟨i, k⟩) = (X F Z) (⟨i, k⟩) \underset{˙}{+} (Y F Z) (⟨i, k⟩)$
102	90 95 98 100 101	syl22anc	$⊢ (φ \land (i \in M \land k \in O)) \to ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) (⟨i, k⟩) = (X F Z) (⟨i, k⟩) \underset{˙}{+} (Y F Z) (⟨i, k⟩)$
103		df-ov	$⊢ i ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) k = ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) (⟨i, k⟩)$
104		df-ov	$⊢ i (X F Z) k = (X F Z) (⟨i, k⟩)$
105		df-ov	$⊢ i (Y F Z) k = (Y F Z) (⟨i, k⟩)$
106	104 105	oveq12i	$⊢ (i (X F Z) k) \underset{˙}{+} (i (Y F Z) k) = (X F Z) (⟨i, k⟩) \underset{˙}{+} (Y F Z) (⟨i, k⟩)$
107	102 103 106	3eqtr4g	$⊢ (φ \land (i \in M \land k \in O)) \to i ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) k = (i (X F Z) k) \underset{˙}{+} (i (Y F Z) k)$
108	79 85 107	3eqtr4d	$⊢ (φ \land (i \in M \land k \in O)) \to i ((X {\underset{˙}{+}}_{f} Y) F Z) k = i ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) k$
109	108	ralrimivva	$⊢ φ \to \forall i \in M \forall k \in O i ((X {\underset{˙}{+}}_{f} Y) F Z) k = i ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) k$
110	1 2 3 4 5 6 83 10	mamucl	$⊢ φ \to (X {\underset{˙}{+}}_{f} Y) F Z \in (B^{(M \times O)})$
111		elmapi	$⊢ (X {\underset{˙}{+}}_{f} Y) F Z \in (B^{(M \times O)}) \to ((X {\underset{˙}{+}}_{f} Y) F Z) : M \times O ⟶ B$
112		ffn	$⊢ ((X {\underset{˙}{+}}_{f} Y) F Z) : M \times O ⟶ B \to ((X {\underset{˙}{+}}_{f} Y) F Z) Fn (M \times O)$
113	110 111 112	3syl	$⊢ φ \to ((X {\underset{˙}{+}}_{f} Y) F Z) Fn (M \times O)$
114	1 7	mndvcl	$⊢ (R \in Mnd \land X F Z \in (B^{(M \times O)}) \land Y F Z \in (B^{(M \times O)})) \to (X F Z) {\underset{˙}{+}}_{f} (Y F Z) \in (B^{(M \times O)})$
115	81 86 91 114	syl3anc	$⊢ φ \to (X F Z) {\underset{˙}{+}}_{f} (Y F Z) \in (B^{(M \times O)})$
116		elmapi	$⊢ (X F Z) {\underset{˙}{+}}_{f} (Y F Z) \in (B^{(M \times O)}) \to ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) : M \times O ⟶ B$
117		ffn	$⊢ ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) : M \times O ⟶ B \to ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) Fn (M \times O)$
118	115 116 117	3syl	$⊢ φ \to ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) Fn (M \times O)$
119		eqfnov2	$⊢ (((X {\underset{˙}{+}}_{f} Y) F Z) Fn (M \times O) \land ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) Fn (M \times O)) \to ((X {\underset{˙}{+}}_{f} Y) F Z = (X F Z) {\underset{˙}{+}}_{f} (Y F Z) \leftrightarrow \forall i \in M \forall k \in O i ((X {\underset{˙}{+}}_{f} Y) F Z) k = i ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) k)$
120	113 118 119	syl2anc	$⊢ φ \to ((X {\underset{˙}{+}}_{f} Y) F Z = (X F Z) {\underset{˙}{+}}_{f} (Y F Z) \leftrightarrow \forall i \in M \forall k \in O i ((X {\underset{˙}{+}}_{f} Y) F Z) k = i ((X F Z) {\underset{˙}{+}}_{f} (Y F Z)) k)$
121	109 120	mpbird	$⊢ φ \to (X {\underset{˙}{+}}_{f} Y) F Z = (X F Z) {\underset{˙}{+}}_{f} (Y F Z)$

Metamath Proof Explorer

Theorem mamudi

Proof