# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
mamuvs2.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
mamuvs2.t
mamuvs2.f ${⊢}{F}={R}\mathrm{maMul}⟨{M},{N},{O}⟩$
mamuvs2.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
mamuvs2.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
mamuvs2.o ${⊢}{\phi }\to {O}\in \mathrm{Fin}$
mamuvs2.x ${⊢}{\phi }\to {X}\in \left({{B}}^{\left({M}×{N}\right)}\right)$
mamuvs2.y ${⊢}{\phi }\to {Y}\in {B}$
mamuvs2.z ${⊢}{\phi }\to {Z}\in \left({{B}}^{\left({N}×{O}\right)}\right)$
Assertion mamuvs2

### Proof

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