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

Proof

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