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 eqid 
 |-  ( +g ` R ) = ( +g ` R )
13 2 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> R e. Ring )
14 5 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> N e. Fin )
15 8 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> X e. B )
16 2 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> R e. Ring )
17 elmapi 
 |-  ( Y e. ( B ^m ( M X. N ) ) -> Y : ( M X. N ) --> B )
18 9 17 syl 
 |-  ( ph -> Y : ( M X. N ) --> B )
19 18 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Y : ( M X. N ) --> B )
20 simplrl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> i e. M )
21 simpr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> j e. N )
22 19 20 21 fovrnd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( i Y j ) e. B )
23 elmapi 
 |-  ( Z e. ( B ^m ( N X. O ) ) -> Z : ( N X. O ) --> B )
24 10 23 syl 
 |-  ( ph -> Z : ( N X. O ) --> B )
25 24 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Z : ( N X. O ) --> B )
26 simplrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> k e. O )
27 25 21 26 fovrnd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( j Z k ) e. B )
28 1 7 ringcl 
 |-  ( ( R e. Ring /\ ( i Y j ) e. B /\ ( j Z k ) e. B ) -> ( ( i Y j ) .x. ( j Z k ) ) e. B )
29 16 22 27 28 syl3anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i Y j ) .x. ( j Z k ) ) e. B )
30 eqid 
 |-  ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) ) = ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) )
31 ovexd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i Y j ) .x. ( j Z k ) ) e. _V )
32 fvexd 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( 0g ` R ) e. _V )
33 30 14 31 32 fsuppmptdm 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) ) finSupp ( 0g ` R ) )
34 1 11 12 7 13 14 15 29 33 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 ) ) ) ) ) )
35 df-ov 
 |-  ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) = ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) ` <. i , j >. )
36 simprl 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> i e. M )
37 opelxpi 
 |-  ( ( i e. M /\ j e. N ) -> <. i , j >. e. ( M X. N ) )
38 36 37 sylan 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> <. i , j >. e. ( M X. N ) )
39 xpfi 
 |-  ( ( M e. Fin /\ N e. Fin ) -> ( M X. N ) e. Fin )
40 4 5 39 syl2anc 
 |-  ( ph -> ( M X. N ) e. Fin )
41 40 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( M X. N ) e. Fin )
42 8 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> X e. B )
43 ffn 
 |-  ( Y : ( M X. N ) --> B -> Y Fn ( M X. N ) )
44 9 17 43 3syl 
 |-  ( ph -> Y Fn ( M X. N ) )
45 44 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Y Fn ( M X. N ) )
46 df-ov 
 |-  ( i Y j ) = ( Y ` <. i , j >. )
47 46 eqcomi 
 |-  ( Y ` <. i , j >. ) = ( i Y j )
48 47 a1i 
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) /\ <. i , j >. e. ( M X. N ) ) -> ( Y ` <. i , j >. ) = ( i Y j ) )
49 41 42 45 48 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 ) ) )
50 38 49 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 ) ) )
51 35 50 syl5eq 
 |-  ( ( ( 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 ) ) )
52 51 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 ) ) )
53 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 ) ) ) )
54 16 42 22 27 53 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 ) ) ) )
55 52 54 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 ) ) ) )
56 55 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 ) ) ) ) )
57 56 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 ) ) ) ) ) )
58 4 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> M e. Fin )
59 6 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> O e. Fin )
60 9 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> Y e. ( B ^m ( M X. N ) ) )
61 10 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> Z e. ( B ^m ( N X. O ) ) )
62 simprr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> k e. O )
63 3 1 7 13 58 14 59 60 61 36 62 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 ) ) ) ) )
64 63 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 ) ) ) ) ) )
65 34 57 64 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 ) ) )
66 fconst6g 
 |-  ( X e. B -> ( ( M X. N ) X. { X } ) : ( M X. N ) --> B )
67 8 66 syl 
 |-  ( ph -> ( ( M X. N ) X. { X } ) : ( M X. N ) --> B )
68 1 fvexi 
 |-  B e. _V
69 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 ) )
70 68 40 69 sylancr 
 |-  ( ph -> ( ( ( M X. N ) X. { X } ) e. ( B ^m ( M X. N ) ) <-> ( ( M X. N ) X. { X } ) : ( M X. N ) --> B ) )
71 67 70 mpbird 
 |-  ( ph -> ( ( M X. N ) X. { X } ) e. ( B ^m ( M X. N ) ) )
72 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 ) ) )
73 2 71 9 72 syl3anc 
 |-  ( ph -> ( ( ( M X. N ) X. { X } ) oF .x. Y ) e. ( B ^m ( M X. N ) ) )
74 73 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( ( ( M X. N ) X. { X } ) oF .x. Y ) e. ( B ^m ( M X. N ) ) )
75 3 1 7 13 58 14 59 74 61 36 62 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 ) ) ) ) )
76 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 >. )
77 opelxpi 
 |-  ( ( i e. M /\ k e. O ) -> <. i , k >. e. ( M X. O ) )
78 77 adantl 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> <. i , k >. e. ( M X. O ) )
79 xpfi 
 |-  ( ( M e. Fin /\ O e. Fin ) -> ( M X. O ) e. Fin )
80 4 6 79 syl2anc 
 |-  ( ph -> ( M X. O ) e. Fin )
81 80 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( M X. O ) e. Fin )
82 1 2 3 4 5 6 9 10 mamucl 
 |-  ( ph -> ( Y F Z ) e. ( B ^m ( M X. O ) ) )
83 elmapi 
 |-  ( ( Y F Z ) e. ( B ^m ( M X. O ) ) -> ( Y F Z ) : ( M X. O ) --> B )
84 ffn 
 |-  ( ( Y F Z ) : ( M X. O ) --> B -> ( Y F Z ) Fn ( M X. O ) )
85 82 83 84 3syl 
 |-  ( ph -> ( Y F Z ) Fn ( M X. O ) )
86 85 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( Y F Z ) Fn ( M X. O ) )
87 df-ov 
 |-  ( i ( Y F Z ) k ) = ( ( Y F Z ) ` <. i , k >. )
88 87 eqcomi 
 |-  ( ( Y F Z ) ` <. i , k >. ) = ( i ( Y F Z ) k )
89 88 a1i 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ <. i , k >. e. ( M X. O ) ) -> ( ( Y F Z ) ` <. i , k >. ) = ( i ( Y F Z ) k ) )
90 81 15 86 89 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 ) ) )
91 78 90 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 ) ) )
92 76 91 syl5eq 
 |-  ( ( 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 ) ) )
93 65 75 92 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 ) )
94 93 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 ) )
95 1 2 3 4 5 6 73 10 mamucl 
 |-  ( ph -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) e. ( B ^m ( M X. O ) ) )
96 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 )
97 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 ) )
98 95 96 97 3syl 
 |-  ( ph -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) Fn ( M X. O ) )
99 fconst6g 
 |-  ( X e. B -> ( ( M X. O ) X. { X } ) : ( M X. O ) --> B )
100 8 99 syl 
 |-  ( ph -> ( ( M X. O ) X. { X } ) : ( M X. O ) --> B )
101 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 ) )
102 68 80 101 sylancr 
 |-  ( ph -> ( ( ( M X. O ) X. { X } ) e. ( B ^m ( M X. O ) ) <-> ( ( M X. O ) X. { X } ) : ( M X. O ) --> B ) )
103 100 102 mpbird 
 |-  ( ph -> ( ( M X. O ) X. { X } ) e. ( B ^m ( M X. O ) ) )
104 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 ) ) )
105 2 103 82 104 syl3anc 
 |-  ( ph -> ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) e. ( B ^m ( M X. O ) ) )
106 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 )
107 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 ) )
108 105 106 107 3syl 
 |-  ( ph -> ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) Fn ( M X. O ) )
109 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 ) ) )
110 98 108 109 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 ) ) )
111 94 110 mpbird 
 |-  ( ph -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) = ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) )