# Metamath Proof Explorer

## Theorem mamuvs1

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

Ref Expression
Hypotheses mamucl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
mamucl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
mamudi.f ${⊢}{F}={R}\mathrm{maMul}⟨{M},{N},{O}⟩$
mamudi.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
mamudi.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
mamudi.o ${⊢}{\phi }\to {O}\in \mathrm{Fin}$
mamuvs1.t
mamuvs1.x ${⊢}{\phi }\to {X}\in {B}$
mamuvs1.y ${⊢}{\phi }\to {Y}\in \left({{B}}^{\left({M}×{N}\right)}\right)$
mamuvs1.z ${⊢}{\phi }\to {Z}\in \left({{B}}^{\left({N}×{O}\right)}\right)$
Assertion mamuvs1

### Proof

Step Hyp Ref Expression
1 mamucl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 mamucl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
3 mamudi.f ${⊢}{F}={R}\mathrm{maMul}⟨{M},{N},{O}⟩$
4 mamudi.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
5 mamudi.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
6 mamudi.o ${⊢}{\phi }\to {O}\in \mathrm{Fin}$
7 mamuvs1.t
8 mamuvs1.x ${⊢}{\phi }\to {X}\in {B}$
9 mamuvs1.y ${⊢}{\phi }\to {Y}\in \left({{B}}^{\left({M}×{N}\right)}\right)$
10 mamuvs1.z ${⊢}{\phi }\to {Z}\in \left({{B}}^{\left({N}×{O}\right)}\right)$
11 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
12 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
13 2 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {R}\in \mathrm{Ring}$
14 5 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {N}\in \mathrm{Fin}$
15 8 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {X}\in {B}$
16 2 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {R}\in \mathrm{Ring}$
17 elmapi ${⊢}{Y}\in \left({{B}}^{\left({M}×{N}\right)}\right)\to {Y}:{M}×{N}⟶{B}$
18 9 17 syl ${⊢}{\phi }\to {Y}:{M}×{N}⟶{B}$
19 18 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {Y}:{M}×{N}⟶{B}$
20 simplrl ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {i}\in {M}$
21 simpr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {j}\in {N}$
22 19 20 21 fovrnd ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {i}{Y}{j}\in {B}$
23 elmapi ${⊢}{Z}\in \left({{B}}^{\left({N}×{O}\right)}\right)\to {Z}:{N}×{O}⟶{B}$
24 10 23 syl ${⊢}{\phi }\to {Z}:{N}×{O}⟶{B}$
25 24 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {Z}:{N}×{O}⟶{B}$
26 simplrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {k}\in {O}$
27 25 21 26 fovrnd ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {j}{Z}{k}\in {B}$
28 1 7 ringcl
29 16 22 27 28 syl3anc
30 eqid
31 ovexd
32 fvexd ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {0}_{{R}}\in \mathrm{V}$
33 30 14 31 32 fsuppmptdm
34 1 11 12 7 13 14 15 29 33 gsummulc2
35 df-ov
36 simprl ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {i}\in {M}$
37 opelxpi ${⊢}\left({i}\in {M}\wedge {j}\in {N}\right)\to ⟨{i},{j}⟩\in \left({M}×{N}\right)$
38 36 37 sylan ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to ⟨{i},{j}⟩\in \left({M}×{N}\right)$
39 xpfi ${⊢}\left({M}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to {M}×{N}\in \mathrm{Fin}$
40 4 5 39 syl2anc ${⊢}{\phi }\to {M}×{N}\in \mathrm{Fin}$
41 40 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {M}×{N}\in \mathrm{Fin}$
42 8 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {X}\in {B}$
43 ffn ${⊢}{Y}:{M}×{N}⟶{B}\to {Y}Fn\left({M}×{N}\right)$
44 9 17 43 3syl ${⊢}{\phi }\to {Y}Fn\left({M}×{N}\right)$
45 44 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\to {Y}Fn\left({M}×{N}\right)$
46 df-ov ${⊢}{i}{Y}{j}={Y}\left(⟨{i},{j}⟩\right)$
47 46 eqcomi ${⊢}{Y}\left(⟨{i},{j}⟩\right)={i}{Y}{j}$
48 47 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge {j}\in {N}\right)\wedge ⟨{i},{j}⟩\in \left({M}×{N}\right)\right)\to {Y}\left(⟨{i},{j}⟩\right)={i}{Y}{j}$
49 41 42 45 48 ofc1
50 38 49 mpdan
51 35 50 syl5eq
52 51 oveq1d
53 1 7 ringass
54 16 42 22 27 53 syl13anc
55 52 54 eqtrd
56 55 mpteq2dva
57 56 oveq2d
58 4 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {M}\in \mathrm{Fin}$
59 6 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {O}\in \mathrm{Fin}$
60 9 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {Y}\in \left({{B}}^{\left({M}×{N}\right)}\right)$
61 10 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {Z}\in \left({{B}}^{\left({N}×{O}\right)}\right)$
62 simprr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {k}\in {O}$
63 3 1 7 13 58 14 59 60 61 36 62 mamufv
64 63 oveq2d
65 34 57 64 3eqtr4d
66 fconst6g ${⊢}{X}\in {B}\to \left(\left({M}×{N}\right)×\left\{{X}\right\}\right):{M}×{N}⟶{B}$
67 8 66 syl ${⊢}{\phi }\to \left(\left({M}×{N}\right)×\left\{{X}\right\}\right):{M}×{N}⟶{B}$
68 1 fvexi ${⊢}{B}\in \mathrm{V}$
69 elmapg ${⊢}\left({B}\in \mathrm{V}\wedge {M}×{N}\in \mathrm{Fin}\right)\to \left(\left({M}×{N}\right)×\left\{{X}\right\}\in \left({{B}}^{\left({M}×{N}\right)}\right)↔\left(\left({M}×{N}\right)×\left\{{X}\right\}\right):{M}×{N}⟶{B}\right)$
70 68 40 69 sylancr ${⊢}{\phi }\to \left(\left({M}×{N}\right)×\left\{{X}\right\}\in \left({{B}}^{\left({M}×{N}\right)}\right)↔\left(\left({M}×{N}\right)×\left\{{X}\right\}\right):{M}×{N}⟶{B}\right)$
71 67 70 mpbird ${⊢}{\phi }\to \left({M}×{N}\right)×\left\{{X}\right\}\in \left({{B}}^{\left({M}×{N}\right)}\right)$
72 1 7 ringvcl
73 2 71 9 72 syl3anc
75 3 1 7 13 58 14 59 74 61 36 62 mamufv
76 df-ov
77 opelxpi ${⊢}\left({i}\in {M}\wedge {k}\in {O}\right)\to ⟨{i},{k}⟩\in \left({M}×{O}\right)$
78 77 adantl ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to ⟨{i},{k}⟩\in \left({M}×{O}\right)$
79 xpfi ${⊢}\left({M}\in \mathrm{Fin}\wedge {O}\in \mathrm{Fin}\right)\to {M}×{O}\in \mathrm{Fin}$
80 4 6 79 syl2anc ${⊢}{\phi }\to {M}×{O}\in \mathrm{Fin}$
81 80 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to {M}×{O}\in \mathrm{Fin}$
82 1 2 3 4 5 6 9 10 mamucl ${⊢}{\phi }\to {Y}{F}{Z}\in \left({{B}}^{\left({M}×{O}\right)}\right)$
83 elmapi ${⊢}{Y}{F}{Z}\in \left({{B}}^{\left({M}×{O}\right)}\right)\to \left({Y}{F}{Z}\right):{M}×{O}⟶{B}$
84 ffn ${⊢}\left({Y}{F}{Z}\right):{M}×{O}⟶{B}\to \left({Y}{F}{Z}\right)Fn\left({M}×{O}\right)$
85 82 83 84 3syl ${⊢}{\phi }\to \left({Y}{F}{Z}\right)Fn\left({M}×{O}\right)$
86 85 adantr ${⊢}\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\to \left({Y}{F}{Z}\right)Fn\left({M}×{O}\right)$
87 df-ov ${⊢}{i}\left({Y}{F}{Z}\right){k}=\left({Y}{F}{Z}\right)\left(⟨{i},{k}⟩\right)$
88 87 eqcomi ${⊢}\left({Y}{F}{Z}\right)\left(⟨{i},{k}⟩\right)={i}\left({Y}{F}{Z}\right){k}$
89 88 a1i ${⊢}\left(\left({\phi }\wedge \left({i}\in {M}\wedge {k}\in {O}\right)\right)\wedge ⟨{i},{k}⟩\in \left({M}×{O}\right)\right)\to \left({Y}{F}{Z}\right)\left(⟨{i},{k}⟩\right)={i}\left({Y}{F}{Z}\right){k}$
90 81 15 86 89 ofc1
91 78 90 mpdan
92 76 91 syl5eq
93 65 75 92 3eqtr4d
94 93 ralrimivva
95 1 2 3 4 5 6 73 10 mamucl
96 elmapi
97 ffn
98 95 96 97 3syl
99 fconst6g ${⊢}{X}\in {B}\to \left(\left({M}×{O}\right)×\left\{{X}\right\}\right):{M}×{O}⟶{B}$
100 8 99 syl ${⊢}{\phi }\to \left(\left({M}×{O}\right)×\left\{{X}\right\}\right):{M}×{O}⟶{B}$
101 elmapg ${⊢}\left({B}\in \mathrm{V}\wedge {M}×{O}\in \mathrm{Fin}\right)\to \left(\left({M}×{O}\right)×\left\{{X}\right\}\in \left({{B}}^{\left({M}×{O}\right)}\right)↔\left(\left({M}×{O}\right)×\left\{{X}\right\}\right):{M}×{O}⟶{B}\right)$
102 68 80 101 sylancr ${⊢}{\phi }\to \left(\left({M}×{O}\right)×\left\{{X}\right\}\in \left({{B}}^{\left({M}×{O}\right)}\right)↔\left(\left({M}×{O}\right)×\left\{{X}\right\}\right):{M}×{O}⟶{B}\right)$
103 100 102 mpbird ${⊢}{\phi }\to \left({M}×{O}\right)×\left\{{X}\right\}\in \left({{B}}^{\left({M}×{O}\right)}\right)$
104 1 7 ringvcl
105 2 103 82 104 syl3anc
106 elmapi
107 ffn
108 105 106 107 3syl
109 eqfnov2
110 98 108 109 syl2anc
111 94 110 mpbird