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		ringcmn	$⊢ R \in Ring \to R \in CMnd$
27	4 26	syl	$⊢ φ \to R \in CMnd$
28	27	adantr	$⊢ (φ \land i \in N) \to R \in CMnd$
29	5	adantr	$⊢ (φ \land i \in N) \to N \in Fin$
30	4	ad2antrr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to R \in Ring$
31		elmapi	$⊢ X \in (B^{(N \times N)}) \to X : N \times N ⟶ B$
32	13 31	syl	$⊢ φ \to X : N \times N ⟶ B$
33	32	ad2antrr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to X : N \times N ⟶ B$
34		simplr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to i \in N$
35		simprr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to k \in N$
36	33 34 35	fovrnd	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to i X k \in B$
37		elmapi	$⊢ Z \in (B^{(N \times N)}) \to Z : N \times N ⟶ B$
38	14 37	syl	$⊢ φ \to Z : N \times N ⟶ B$
39	38	ad2antrr	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to Z : N \times N ⟶ B$
40		simprl	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to j \in N$
41	39 35 40	fovrnd	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to k Z j \in B$
42		elmapi	$⊢ Y \in (B^{N}) \to Y : N ⟶ B$
43		ffvelrn	$⊢ (Y : N ⟶ B \land j \in N) \to Y (j) \in B$
44	43	ex	$⊢ Y : N ⟶ B \to (j \in N \to Y (j) \in B)$
45	6 42 44	3syl	$⊢ φ \to (j \in N \to Y (j) \in B)$
46	45	imp	$⊢ (φ \land j \in N) \to Y (j) \in B$
47	46	ad2ant2r	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to Y (j) \in B$
48	2 10	ringcl	$⊢ (R \in Ring \land k Z j \in B \land Y (j) \in B) \to (k Z j) \cdot_{R} Y (j) \in B$
49	30 41 47 48	syl3anc	$⊢ ((φ \land i \in N) \land (j \in N \land k \in N)) \to (k Z j) \cdot_{R} Y (j) \in B$
50	2 10	ringcl	$⊢ (R \in Ring \land i X k \in B \land (k Z j) \cdot_{R} Y (j) \in B) \to (i X k) \cdot_{R} ((k Z j) \cdot_{R} Y (j)) \in B$
51	30 36 49 50	syl3anc	$⊢ ((φ \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$
52	2 28 29 29 51	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))))$
53	4	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to R \in Ring$
54	5	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to N \in Fin$
55	13	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to X \in (B^{(N \times N)})$
56	14	ad2antrr	$⊢ ((φ \land i \in N) \land j \in N) \to Z \in (B^{(N \times N)})$
57		simplr	$⊢ ((φ \land i \in N) \land j \in N) \to i \in N$
58		simpr	$⊢ ((φ \land i \in N) \land j \in N) \to j \in N$
59	7 2 10 53 54 54 54 55 56 57 58	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))$
60	59	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)$
61		eqid	$⊢ 0_{R} = 0_{R}$
62		eqid	$⊢ +_{R} = +_{R}$
63	46	adantlr	$⊢ ((φ \land i \in N) \land j \in N) \to Y (j) \in B$
64	4	adantr	$⊢ (φ \land i \in N) \to R \in Ring$
65	64	ad2antrr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to R \in Ring$
66	32	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to X : N \times N ⟶ B$
67		simplr	$⊢ ((φ \land i \in N) \land k \in N) \to i \in N$
68		simpr	$⊢ ((φ \land i \in N) \land k \in N) \to k \in N$
69	66 67 68	fovrnd	$⊢ ((φ \land i \in N) \land k \in N) \to i X k \in B$
70	69	adantlr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to i X k \in B$
71	38	adantr	$⊢ (φ \land i \in N) \to Z : N \times N ⟶ B$
72	71	ad2antrr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to Z : N \times N ⟶ B$
73		simpr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to k \in N$
74		simplr	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to j \in N$
75	72 73 74	fovrnd	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to k Z j \in B$
76	2 10	ringcl	$⊢ (R \in Ring \land i X k \in B \land k Z j \in B) \to (i X k) \cdot_{R} (k Z j) \in B$
77	65 70 75 76	syl3anc	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to (i X k) \cdot_{R} (k Z j) \in B$
78		eqid	$⊢ (k \in N ⟼ (i X k) \cdot_{R} (k Z j)) = (k \in N ⟼ (i X k) \cdot_{R} (k Z j))$
79		ovexd	$⊢ (((φ \land i \in N) \land j \in N) \land k \in N) \to (i X k) \cdot_{R} (k Z j) \in V$
80		fvexd	$⊢ ((φ \land i \in N) \land j \in N) \to 0_{R} \in V$
81	78 54 79 80	fsuppmptdm	$⊢ ((φ \land i \in N) \land j \in N) \to {finSupp}_{0_{R}} ((k \in N ⟼ (i X k) \cdot_{R} (k Z j)))$
82	2 61 62 10 53 54 63 77 81	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)$
83	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))$
84	30 36 41 47 83	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))$
85	84	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))$
86	85	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)))$
87	86	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)))$
88	60 82 87	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)))$
89	88	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))))$
90	89	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))))$
91	4	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to R \in Ring$
92	5	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to N \in Fin$
93	9	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to Z \in {Base}_{A}$
94	6	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to Y \in (B^{N})$
95	1 3 2 10 91 92 93 94 68	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))$
96	95	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)))$
97	64	ad2antrr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to R \in Ring$
98	71	ad2antrr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to Z : N \times N ⟶ B$
99		simplr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to k \in N$
100		simpr	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to j \in N$
101	98 99 100	fovrnd	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to k Z j \in B$
102	45	ad2antrr	$⊢ ((φ \land i \in N) \land k \in N) \to (j \in N \to Y (j) \in B)$
103	102	imp	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to Y (j) \in B$
104	97 101 103 48	syl3anc	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to (k Z j) \cdot_{R} Y (j) \in B$
105		eqid	$⊢ (j \in N ⟼ (k Z j) \cdot_{R} Y (j)) = (j \in N ⟼ (k Z j) \cdot_{R} Y (j))$
106		ovexd	$⊢ (((φ \land i \in N) \land k \in N) \land j \in N) \to (k Z j) \cdot_{R} Y (j) \in V$
107		fvexd	$⊢ ((φ \land i \in N) \land k \in N) \to 0_{R} \in V$
108	105 92 106 107	fsuppmptdm	$⊢ ((φ \land i \in N) \land k \in N) \to {finSupp}_{0_{R}} ((j \in N ⟼ (k Z j) \cdot_{R} Y (j)))$
109	2 61 62 10 91 92 69 104 108	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)))$
110	96 109	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)))$
111	110	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))))$
112	111	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))))$
113	52 90 112	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))$
114	16	adantr	$⊢ (φ \land i \in N) \to X \underset{˙}{\times} Z \in {Base}_{A}$
115	6	adantr	$⊢ (φ \land i \in N) \to Y \in (B^{N})$
116		simpr	$⊢ (φ \land i \in N) \to i \in N$
117	1 3 2 10 64 29 114 115 116	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))$
118	8	adantr	$⊢ (φ \land i \in N) \to X \in {Base}_{A}$
119	21	adantr	$⊢ (φ \land i \in N) \to Z \underset{˙}{\cdot} Y \in (B^{N})$
120	1 3 2 10 64 29 118 119 116	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))$
121	113 117 120	3eqtr4d	$⊢ (φ \land i \in N) \to ((X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y) (i) = (X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) (i)$
122	20 25 121	eqfnfvd	$⊢ φ \to (X \underset{˙}{\times} Z) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem mavmulass

Proof