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 φ R CRing
mamuvs2.b B = Base R
mamuvs2.t · ˙ = R
mamuvs2.f F = R maMul M N O
mamuvs2.m φ M Fin
mamuvs2.n φ N Fin
mamuvs2.o φ O Fin
mamuvs2.x φ X B M × N
mamuvs2.y φ Y B
mamuvs2.z φ Z B N × O
Assertion mamuvs2 φ X F N × O × Y · ˙ f Z = M × O × Y · ˙ f X F Z

Proof

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