mavmulass

Description: Associativity of the multiplication of two NxN matrices with an N-dimensional vector. (Contributed by AV, 9-Feb-2019) (Revised by AV, 25-Feb-2019) (Proof shortened by AV, 22-Jul-2019)

	Ref	Expression
Hypotheses	1mavmul.a	$⊢ A = N Mat R$
	1mavmul.b	$⊢ B = {Base}_{R}$
	1mavmul.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
	1mavmul.r	$⊢ φ \to R \in Ring$
	1mavmul.n	$⊢ φ \to N \in Fin$
	1mavmul.y	$⊢ φ \to Y \in (B^{N})$
	mavmulass.m	$⊢ \underset{˙}{\times} = R maMul ⟨N, N, N⟩$
	mavmulass.x	$⊢ φ \to X \in {Base}_{A}$
	mavmulass.z	$⊢ φ \to Z \in {Base}_{A}$
Assertion	mavmulass	$⊢ φ \to (X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		1mavmul.a	$⊢ A = N Mat R$
2		1mavmul.b	$⊢ B = {Base}_{R}$
3		1mavmul.t	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
4		1mavmul.r	$⊢ φ \to R \in Ring$
5		1mavmul.n	$⊢ φ \to N \in Fin$
6		1mavmul.y	$⊢ φ \to Y \in (B^{N})$
7		mavmulass.m	$⊢ \underset{˙}{\times} = R maMul ⟨N, N, N⟩$
8		mavmulass.x	$⊢ φ \to X \in {Base}_{A}$
9		mavmulass.z	$⊢ φ \to Z \in {Base}_{A}$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	1 2	matbas2	$⊢ (N \in Fin \land R \in Ring) \to B^{(N \times N)} = {Base}_{A}$
12	5 4 11	syl2anc	$⊢ φ \to B^{(N \times N)} = {Base}_{A}$
13	8 12	eleqtrrd	$⊢ φ \to X \in (B^{(N \times N)})$
14	9 12	eleqtrrd	$⊢ φ \to Z \in (B^{(N \times N)})$
15	2 4 7 5 5 5 13 14	mamucl	$⊢ φ \to X \underset{˙}{\times} Z \in (B^{(N \times N)})$
16	15 12	eleqtrd	$⊢ φ \to X \underset{˙}{\times} Z \in {Base}_{A}$
17	1 3 2 10 4 5 16 6	mavmulcl	$⊢ φ \to (X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y \in (B^{N})$
18		elmapi	$⊢ (X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y \in (B^{N}) \to ((X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y) : N ⟶ B$
19		ffn	$⊢ ((X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y) : N ⟶ B \to ((X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y) Fn N$
20	17 18 19	3syl	$⊢ φ \to ((X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y) Fn N$
21	1 3 2 10 4 5 9 6	mavmulcl	$⊢ φ \to Z \underset{˙}{\cdot} Y \in (B^{N})$
22	1 3 2 10 4 5 8 21	mavmulcl	$⊢ φ \to X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y) \in (B^{N})$
23		elmapi	$⊢ X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y) \in (B^{N}) \to (X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) : N ⟶ B$
24		ffn	$⊢ (X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) : N ⟶ B \to (X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) Fn N$
25	22 23 24	3syl	$⊢ φ \to (X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) Fn N$
26	4	ringcmnd	$⊢ φ \to R \in CMnd$
27	26	adantr	$⊢ (φ \land i \in N) \to R \in CMnd$
28	5	adantr	$⊢ (φ \land i \in N) \to N \in Fin$
29	4	ad2antrr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to R \in Ring$
30		elmapi	$⊢ X \in (B^{(N \times N)}) \to X : N \times N ⟶ B$
31	13 30	syl	$⊢ φ \to X : N \times N ⟶ B$
32	31	ad2antrr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to X : N \times N ⟶ B$
33		simplr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to i \in N$
34		simprr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to k \in N$
35	32 33 34	fovcdmd	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to i X k \in B$
36		elmapi	$⊢ Z \in (B^{(N \times N)}) \to Z : N \times N ⟶ B$
37	14 36	syl	$⊢ φ \to Z : N \times N ⟶ B$
38	37	ad2antrr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to Z : N \times N ⟶ B$
39		simprl	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to j \in N$
40	38 34 39	fovcdmd	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to k Z j \in B$
41		elmapi	$⊢ Y \in (B^{N}) \to Y : N ⟶ B$
42		ffvelcdm	$⊢ (Y : N ⟶ B \land j \in N) \to Y (j) \in B$
43	42	ex	$⊢ Y : N ⟶ B \to (j \in N \to Y (j) \in B)$
44	6 41 43	3syl	$⊢ φ \to (j \in N \to Y (j) \in B)$
45	44	imp	$⊢ (φ \land j \in N) \to Y (j) \in B$
46	45	ad2ant2r	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to Y (j) \in B$
47	2 10 29 40 46	ringcld	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to (k Z j) \cdot_{R} Y (j) \in B$
48	2 10 29 35 47	ringcld	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to (i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j)) \in B$
49	2 27 28 28 48	gsumcom3fi	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} (\underset{k \in N}{\sum_{R}}, ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j)))) = \underset{k \in N}{\sum_{R}} (\underset{j \in N}{\sum_{R}}, ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))))$
50	4	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to R \in Ring$
51	5	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to N \in Fin$
52	13	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to X \in (B^{(N \times N)})$
53	14	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to Z \in (B^{(N \times N)})$
54		simplr	$⊢ ((φ \land i \in N) \land j \in N) \to i \in N$
55		simpr	$⊢ ((φ \land i \in N) \land j \in N) \to j \in N$
56	7 2 10 50 51 51 51 52 53 54 55	mamufv	$⊢ ((φ \land i \in N) \land j \in N) \to i (X \underset{˙}{\times} Z) j = \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Z j))$
57	56	oveq1d	$⊢ ((φ \land i \in N) \land j \in N) \to (i (X \underset{˙}{\times} Z) j) \cdot_{R} Y (j) = (\underset{k \in N}{\sum_{R}}, ((i X k) \cdot_{R} (k Z j))) \cdot_{R} Y (j)$
58		eqid	$⊢ 0_{R} = 0_{R}$
59	45	adantlr	$⊢ ((φ \land i \in N) \land j \in N) \to Y (j) \in B$
60	4	adantr	$⊢ (φ \land i \in N) \to R \in Ring$
61	60	ad2antrr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to R \in Ring$
62	31	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to X : N \times N ⟶ B$
63		simplr	$⊢ ((φ \land i \in N) \land k \in N) \to i \in N$
64		simpr	$⊢ ((φ \land i \in N) \land k \in N) \to k \in N$
65	62 63 64	fovcdmd	$⊢ ((φ \land i \in N) \land k \in N) \to i X k \in B$
66	65	adantlr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to i X k \in B$
67	37	adantr	$⊢ (φ \land i \in N) \to Z : N \times N ⟶ B$
68	67	ad2antrr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to Z : N \times N ⟶ B$
69		simpr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to k \in N$
70		simplr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to j \in N$
71	68 69 70	fovcdmd	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to k Z j \in B$
72	2 10 61 66 71	ringcld	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to (i X k) \cdot_{R} (k Z j) \in B$
73		eqid	$⊢ (k \in N ⟼ (i X k) \cdot_{R} (k Z j)) = (k \in N ⟼ (i X k) \cdot_{R} (k Z j))$
74		ovexd	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to (i X k) \cdot_{R} (k Z j) \in V$
75		fvexd	$⊢ ((φ \land i \in N) \land j \in N) \to 0_{R} \in V$
76	73 51 74 75	fsuppmptdm	$⊢ ((φ \land i \in N) \land j \in N) \to {finSupp}_{0_{R}} ((k \in N ⟼ (i X k) \cdot_{R} (k Z j)))$
77	2 58 10 50 51 59 72 76	gsummulc1	$⊢ ((φ \land i \in N) \land j \in N) \to \underset{k \in N}{\sum_{R}} (((i X k) \cdot_{R} (k Z j)) \cdot_{R} Y (j)) = (\underset{k \in N}{\sum_{R}}, ((i X k) \cdot_{R} (k Z j))) \cdot_{R} Y (j)$
78	2 10	ringass	$⊢ (R \in Ring \land (i X k \in B \land k Z j \in B \land Y (j) \in B)) \to ((i X k) \cdot_{R} (k Z j)) \cdot_{R} Y (j) = (i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))$
79	29 35 40 46 78	syl13anc	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to ((i X k) \cdot_{R} (k Z j)) \cdot_{R} Y (j) = (i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))$
80	79	anassrs	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to ((i X k) \cdot_{R} (k Z j)) \cdot_{R} Y (j) = (i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))$
81	80	mpteq2dva	$⊢ ((φ \land i \in N) \land j \in N) \to (k \in N ⟼ ((i X k) \cdot_{R} (k Z j)) \cdot_{R} Y (j)) = (k \in N ⟼ (i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j)))$
82	81	oveq2d	$⊢ ((φ \land i \in N) \land j \in N) \to \underset{k \in N}{\sum_{R}} (((i X k) \cdot_{R} (k Z j)) \cdot_{R} Y (j)) = \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j)))$
83	57 77 82	3eqtr2d	$⊢ ((φ \land i \in N) \land j \in N) \to (i (X \underset{˙}{\times} Z) j) \cdot_{R} Y (j) = \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j)))$
84	83	mpteq2dva	$⊢ (φ \land i \in N) \to (j \in N ⟼ (i (X \underset{˙}{\times} Z) j) \cdot_{R} Y (j)) = (j \in N ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))))$
85	84	oveq2d	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} ((i (X \underset{˙}{\times} Z) j) \cdot_{R} Y (j)) = \underset{j \in N}{\sum_{R}} (\underset{k \in N}{\sum_{R}}, ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))))$
86	4	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to R \in Ring$
87	5	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to N \in Fin$
88	9	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to Z \in {Base}_{A}$
89	6	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to Y \in (B^{N})$
90	1 3 2 10 86 87 88 89 64	mavmulfv	$⊢ ((φ \land i \in N) \land k \in N) \to (Z \underset{˙}{\cdot} Y) (k) = \underset{j \in N}{\sum_{R}} ((k Z j) \cdot_{R} Y (j))$
91	90	oveq2d	$⊢ ((φ \land i \in N) \land k \in N) \to (i X k) \cdot_{R} (Z \underset{˙}{\cdot} Y) (k) = (i X k) \cdot_{R} (\underset{j \in N}{\sum_{R}}, ((k Z j) \cdot_{R} Y (j)))$
92	60	ad2antrr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to R \in Ring$
93	67	ad2antrr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to Z : N \times N ⟶ B$
94		simplr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to k \in N$
95		simpr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to j \in N$
96	93 94 95	fovcdmd	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to k Z j \in B$
97	44	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to (j \in N \to Y (j) \in B)$
98	97	imp	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to Y (j) \in B$
99	2 10 92 96 98	ringcld	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to (k Z j) \cdot_{R} Y (j) \in B$
100		eqid	$⊢ (j \in N ⟼ (k Z j) \cdot_{R} Y (j)) = (j \in N ⟼ (k Z j) \cdot_{R} Y (j))$
101		ovexd	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to (k Z j) \cdot_{R} Y (j) \in V$
102		fvexd	$⊢ ((φ \land i \in N) \land k \in N) \to 0_{R} \in V$
103	100 87 101 102	fsuppmptdm	$⊢ ((φ \land i \in N) \land k \in N) \to {finSupp}_{0_{R}} ((j \in N ⟼ (k Z j) \cdot_{R} Y (j)))$
104	2 58 10 86 87 65 99 103	gsummulc2	$⊢ ((φ \land i \in N) \land k \in N) \to \underset{j \in N}{\sum_{R}} ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))) = (i X k) \cdot_{R} (\underset{j \in N}{\sum_{R}}, ((k Z j) \cdot_{R} Y (j)))$
105	91 104	eqtr4d	$⊢ ((φ \land i \in N) \land k \in N) \to (i X k) \cdot_{R} (Z \underset{˙}{\cdot} Y) (k) = \underset{j \in N}{\sum_{R}} ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j)))$
106	105	mpteq2dva	$⊢ (φ \land i \in N) \to (k \in N ⟼ (i X k) \cdot_{R} (Z \underset{˙}{\cdot} Y) (k)) = (k \in N ⟼ \underset{j \in N}{\sum_{R}} ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))))$
107	106	oveq2d	$⊢ (φ \land i \in N) \to \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (Z \underset{˙}{\cdot} Y) (k)) = \underset{k \in N}{\sum_{R}} (\underset{j \in N}{\sum_{R}}, ((i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j))))$
108	49 85 107	3eqtr4d	$⊢ (φ \land i \in N) \to \underset{j \in N}{\sum_{R}} ((i (X \underset{˙}{\times} Z) j) \cdot_{R} Y (j)) = \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (Z \underset{˙}{\cdot} Y) (k))$
109	16	adantr	$⊢ (φ \land i \in N) \to X \underset{˙}{\times} Z \in {Base}_{A}$
110	6	adantr	$⊢ (φ \land i \in N) \to Y \in (B^{N})$
111		simpr	$⊢ (φ \land i \in N) \to i \in N$
112	1 3 2 10 60 28 109 110 111	mavmulfv	$⊢ (φ \land i \in N) \to ((X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y) (i) = \underset{j \in N}{\sum_{R}} ((i (X \underset{˙}{\times} Z) j) \cdot_{R} Y (j))$
113	8	adantr	$⊢ (φ \land i \in N) \to X \in {Base}_{A}$
114	21	adantr	$⊢ (φ \land i \in N) \to Z \underset{˙}{\cdot} Y \in (B^{N})$
115	1 3 2 10 60 28 113 114 111	mavmulfv	$⊢ (φ \land i \in N) \to (X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) (i) = \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (Z \underset{˙}{\cdot} Y) (k))$
116	108 112 115	3eqtr4d	$⊢ (φ \land i \in N) \to ((X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y) (i) = (X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) (i)$
117	20 25 116	eqfnfvd	$⊢ φ \to (X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem mavmulass

Proof