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	syl5eq	$⊢ ((φ \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	fovrnd	$⊢ ((φ \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	fovrnd	$⊢ ((φ \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		eqid	$⊢ +_{R} = +_{R}$
52		crngring	$⊢ R \in CRing \to R \in Ring$
53	1 52	syl	$⊢ φ \to R \in Ring$
54	53	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to R \in Ring$
55	6	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to N \in Fin$
56	9	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Y \in B$
57	53	ad2antrr	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to R \in Ring$
58	2 3	ringcl	$⊢ (R \in Ring \land i X j \in B \land j Z k \in B) \to (i X j) \underset{˙}{\cdot} (j Z k) \in B$
59	57 39 42 58	syl3anc	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i X j) \underset{˙}{\cdot} (j Z k) \in B$
60		eqid	$⊢ (j \in N ⟼ (i X j) \underset{˙}{\cdot} (j Z k)) = (j \in N ⟼ (i X j) \underset{˙}{\cdot} (j Z k))$
61		ovexd	$⊢ ((φ \land (i \in M \land k \in O)) \land j \in N) \to (i X j) \underset{˙}{\cdot} (j Z k) \in V$
62		fvexd	$⊢ (φ \land (i \in M \land k \in O)) \to 0_{R} \in V$
63	60 55 61 62	fsuppmptdm	$⊢ (φ \land (i \in M \land k \in O)) \to {finSupp}_{0_{R}} ((j \in N ⟼ (i X j) \underset{˙}{\cdot} (j Z k)))$
64	2 50 51 3 54 55 56 59 63	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)))$
65	49 64	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)))$
66	1	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to R \in CRing$
67	5	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \in Fin$
68	7	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to O \in Fin$
69	8	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to X \in (B^{(M \times N)})$
70		fconst6g	$⊢ Y \in B \to ((N \times O) \times \{Y\}) : N \times O ⟶ B$
71	9 70	syl	$⊢ φ \to ((N \times O) \times \{Y\}) : N \times O ⟶ B$
72	2	fvexi	$⊢ B \in V$
73		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)$
74	72 17 73	sylancr	$⊢ φ \to ((N \times O) \times \{Y\} \in (B^{(N \times O)}) \leftrightarrow ((N \times O) \times \{Y\}) : N \times O ⟶ B)$
75	71 74	mpbird	$⊢ φ \to (N \times O) \times \{Y\} \in (B^{(N \times O)})$
76	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)})$
77	53 75 10 76	syl3anc	$⊢ φ \to ((N \times O) \times \{Y\}) {\underset{˙}{\cdot}}_{f} Z \in (B^{(N \times O)})$
78	77	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to ((N \times O) \times \{Y\}) {\underset{˙}{\cdot}}_{f} Z \in (B^{(N \times O)})$
79		simprl	$⊢ (φ \land (i \in M \land k \in O)) \to i \in M$
80		simprr	$⊢ (φ \land (i \in M \land k \in O)) \to k \in O$
81	4 2 3 66 67 55 68 69 78 79 80	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))$
82		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⟩)$
83		opelxpi	$⊢ (i \in M \land k \in O) \to ⟨i, k⟩ \in (M \times O)$
84	83	adantl	$⊢ (φ \land (i \in M \land k \in O)) \to ⟨i, k⟩ \in (M \times O)$
85		xpfi	$⊢ (M \in Fin \land O \in Fin) \to M \times O \in Fin$
86	5 7 85	syl2anc	$⊢ φ \to M \times O \in Fin$
87	86	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to M \times O \in Fin$
88	2 53 4 5 6 7 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		df-ov	$⊢ i (X F Z) k = (X F Z) (⟨i, k⟩)$
94	10	adantr	$⊢ (φ \land (i \in M \land k \in O)) \to Z \in (B^{(N \times O)})$
95	4 2 3 66 67 55 68 69 94 79 80	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))$
96	93 95	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))$
97	96	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))$
98	87 56 92 97	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)))$
99	84 98	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)))$
100	82 99	syl5eq	$⊢ (φ \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)))$
101	65 81 100	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$
102	101	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$
103	2 53 4 5 6 7 8 77	mamucl	$⊢ φ \to X F (((N \times O) \times \{Y\}) {\underset{˙}{\cdot}}_{f} Z) \in (B^{(M \times O)})$
104		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$
105		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)$
106	103 104 105	3syl	$⊢ φ \to (X F (((N \times O) \times \{Y\}) {\underset{˙}{\cdot}}_{f} Z)) Fn (M \times O)$
107		fconst6g	$⊢ Y \in B \to ((M \times O) \times \{Y\}) : M \times O ⟶ B$
108	9 107	syl	$⊢ φ \to ((M \times O) \times \{Y\}) : M \times O ⟶ B$
109		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)$
110	72 86 109	sylancr	$⊢ φ \to ((M \times O) \times \{Y\} \in (B^{(M \times O)}) \leftrightarrow ((M \times O) \times \{Y\}) : M \times O ⟶ B)$
111	108 110	mpbird	$⊢ φ \to (M \times O) \times \{Y\} \in (B^{(M \times O)})$
112	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)})$
113	53 111 88 112	syl3anc	$⊢ φ \to ((M \times O) \times \{Y\}) {\underset{˙}{\cdot}}_{f} (X F Z) \in (B^{(M \times O)})$
114		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$
115		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)$
116	113 114 115	3syl	$⊢ φ \to (((M \times O) \times \{Y\}) {\underset{˙}{\cdot}}_{f} (X F Z)) Fn (M \times O)$
117		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)$
118	106 116 117	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)$
119	102 118	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