# Metamath Proof Explorer

## Theorem 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}\mathrm{Mat}{R}$
1mavmul.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
1mavmul.t
1mavmul.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
1mavmul.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
1mavmul.y ${⊢}{\phi }\to {Y}\in \left({{B}}^{{N}}\right)$
mavmulass.m
mavmulass.x ${⊢}{\phi }\to {X}\in {\mathrm{Base}}_{{A}}$
mavmulass.z ${⊢}{\phi }\to {Z}\in {\mathrm{Base}}_{{A}}$
Assertion mavmulass

### Proof

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