mamuvs2

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

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

Proof

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

Metamath Proof Explorer

Theorem mamuvs2

Proof