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 
|- ( ph -> R e. CRing )
mamuvs2.b 
|- B = ( Base ` R )
mamuvs2.t 
|- .x. = ( .r ` R )
mamuvs2.f 
|- F = ( R maMul <. M , N , O >. )
mamuvs2.m 
|- ( ph -> M e. Fin )
mamuvs2.n 
|- ( ph -> N e. Fin )
mamuvs2.o 
|- ( ph -> O e. Fin )
mamuvs2.x 
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
mamuvs2.y 
|- ( ph -> Y e. B )
mamuvs2.z 
|- ( ph -> Z e. ( B ^m ( N X. O ) ) )
Assertion mamuvs2 
|- ( ph -> ( X F ( ( ( N X. O ) X. { Y } ) oF .x. Z ) ) = ( ( ( M X. O ) X. { Y } ) oF .x. ( X F Z ) ) )

Proof

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