mamudir

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

Metamath Proof Explorer

Theorem mamudir

Proof