Metamath Proof Explorer

Theorem mvmulfval

Description: Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019)

Ref Expression
Hypotheses mvmulfval.x 
|- .X. = ( R maVecMul <. M , N >. )
mvmulfval.b 
|- B = ( Base ` R )
mvmulfval.t 
|- .x. = ( .r ` R )
mvmulfval.r 
|- ( ph -> R e. V )
mvmulfval.m 
|- ( ph -> M e. Fin )
mvmulfval.n 
|- ( ph -> N e. Fin )
Assertion mvmulfval 
|- ( ph -> .X. = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mvmulfval.x 
 |-  .X. = ( R maVecMul <. M , N >. )
2 mvmulfval.b 
 |-  B = ( Base ` R )
3 mvmulfval.t 
 |-  .x. = ( .r ` R )
4 mvmulfval.r 
 |-  ( ph -> R e. V )
5 mvmulfval.m 
 |-  ( ph -> M e. Fin )
6 mvmulfval.n 
 |-  ( ph -> N e. Fin )
7 df-mvmul 
 |-  maVecMul = ( r e. _V , o e. _V |-> [_ ( 1st ` o ) / m ]_ [_ ( 2nd ` o ) / n ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) )
8 7 a1i 
 |-  ( ph -> maVecMul = ( r e. _V , o e. _V |-> [_ ( 1st ` o ) / m ]_ [_ ( 2nd ` o ) / n ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) ) )
9 fvex 
 |-  ( 1st ` o ) e. _V
10 fvex 
 |-  ( 2nd ` o ) e. _V
11 xpeq12 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> ( m X. n ) = ( ( 1st ` o ) X. ( 2nd ` o ) ) )
12 11 oveq2d 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> ( ( Base ` r ) ^m ( m X. n ) ) = ( ( Base ` r ) ^m ( ( 1st ` o ) X. ( 2nd ` o ) ) ) )
13 oveq2 
 |-  ( n = ( 2nd ` o ) -> ( ( Base ` r ) ^m n ) = ( ( Base ` r ) ^m ( 2nd ` o ) ) )
14 13 adantl 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> ( ( Base ` r ) ^m n ) = ( ( Base ` r ) ^m ( 2nd ` o ) ) )
15 simpl 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> m = ( 1st ` o ) )
16 simpr 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> n = ( 2nd ` o ) )
17 16 mpteq1d 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) = ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) )
18 17 oveq2d 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) = ( r gsum ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) )
19 15 18 mpteq12dv 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) = ( i e. ( 1st ` o ) |-> ( r gsum ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) )
20 12 14 19 mpoeq123dv 
 |-  ( ( m = ( 1st ` o ) /\ n = ( 2nd ` o ) ) -> ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) = ( x e. ( ( Base ` r ) ^m ( ( 1st ` o ) X. ( 2nd ` o ) ) ) , y e. ( ( Base ` r ) ^m ( 2nd ` o ) ) |-> ( i e. ( 1st ` o ) |-> ( r gsum ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) )
21 9 10 20 csbie2 
 |-  [_ ( 1st ` o ) / m ]_ [_ ( 2nd ` o ) / n ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) = ( x e. ( ( Base ` r ) ^m ( ( 1st ` o ) X. ( 2nd ` o ) ) ) , y e. ( ( Base ` r ) ^m ( 2nd ` o ) ) |-> ( i e. ( 1st ` o ) |-> ( r gsum ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) )
22 simprl 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> r = R )
23 22 fveq2d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( Base ` r ) = ( Base ` R ) )
24 23 2 eqtr4di 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( Base ` r ) = B )
25 fveq2 
 |-  ( o = <. M , N >. -> ( 1st ` o ) = ( 1st ` <. M , N >. ) )
26 25 ad2antll 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( 1st ` o ) = ( 1st ` <. M , N >. ) )
27 op1stg 
 |-  ( ( M e. Fin /\ N e. Fin ) -> ( 1st ` <. M , N >. ) = M )
28 5 6 27 syl2anc 
 |-  ( ph -> ( 1st ` <. M , N >. ) = M )
29 28 adantr 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( 1st ` <. M , N >. ) = M )
30 26 29 eqtrd 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( 1st ` o ) = M )
31 fveq2 
 |-  ( o = <. M , N >. -> ( 2nd ` o ) = ( 2nd ` <. M , N >. ) )
32 31 ad2antll 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( 2nd ` o ) = ( 2nd ` <. M , N >. ) )
33 op2ndg 
 |-  ( ( M e. Fin /\ N e. Fin ) -> ( 2nd ` <. M , N >. ) = N )
34 5 6 33 syl2anc 
 |-  ( ph -> ( 2nd ` <. M , N >. ) = N )
35 34 adantr 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( 2nd ` <. M , N >. ) = N )
36 32 35 eqtrd 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( 2nd ` o ) = N )
37 30 36 xpeq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( ( 1st ` o ) X. ( 2nd ` o ) ) = ( M X. N ) )
38 24 37 oveq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( ( Base ` r ) ^m ( ( 1st ` o ) X. ( 2nd ` o ) ) ) = ( B ^m ( M X. N ) ) )
39 24 36 oveq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( ( Base ` r ) ^m ( 2nd ` o ) ) = ( B ^m N ) )
40 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
41 40 adantr 
 |-  ( ( r = R /\ o = <. M , N >. ) -> ( .r ` r ) = ( .r ` R ) )
42 41 adantl 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( .r ` r ) = ( .r ` R ) )
43 42 3 eqtr4di 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( .r ` r ) = .x. )
44 43 oveqd 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( ( i x j ) ( .r ` r ) ( y ` j ) ) = ( ( i x j ) .x. ( y ` j ) ) )
45 36 44 mpteq12dv 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) = ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) )
46 22 45 oveq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( r gsum ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) = ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) )
47 30 46 mpteq12dv 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( i e. ( 1st ` o ) |-> ( r gsum ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) = ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) )
48 38 39 47 mpoeq123dv 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> ( x e. ( ( Base ` r ) ^m ( ( 1st ` o ) X. ( 2nd ` o ) ) ) , y e. ( ( Base ` r ) ^m ( 2nd ` o ) ) |-> ( i e. ( 1st ` o ) |-> ( r gsum ( j e. ( 2nd ` o ) |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) )
49 21 48 syl5eq 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N >. ) ) -> [_ ( 1st ` o ) / m ]_ [_ ( 2nd ` o ) / n ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) )
50 4 elexd 
 |-  ( ph -> R e. _V )
51 opex 
 |-  <. M , N >. e. _V
52 51 a1i 
 |-  ( ph -> <. M , N >. e. _V )
53 ovex 
 |-  ( B ^m ( M X. N ) ) e. _V
54 ovex 
 |-  ( B ^m N ) e. _V
55 53 54 mpoex 
 |-  ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) e. _V
56 55 a1i 
 |-  ( ph -> ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) e. _V )
57 8 49 50 52 56 ovmpod 
 |-  ( ph -> ( R maVecMul <. M , N >. ) = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) )
58 1 57 syl5eq 
 |-  ( ph -> .X. = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) )