Metamath Proof Explorer

Theorem mamufval

Description: Functional value of the matrix multiplication operator. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Hypotheses mamufval.f 
|- F = ( R maMul <. M , N , P >. )
mamufval.b 
|- B = ( Base ` R )
mamufval.t 
|- .x. = ( .r ` R )
mamufval.r 
|- ( ph -> R e. V )
mamufval.m 
|- ( ph -> M e. Fin )
mamufval.n 
|- ( ph -> N e. Fin )
mamufval.p 
|- ( ph -> P e. Fin )
Assertion mamufval 
|- ( ph -> F = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mamufval.f 
 |-  F = ( R maMul <. M , N , P >. )
2 mamufval.b 
 |-  B = ( Base ` R )
3 mamufval.t 
 |-  .x. = ( .r ` R )
4 mamufval.r 
 |-  ( ph -> R e. V )
5 mamufval.m 
 |-  ( ph -> M e. Fin )
6 mamufval.n 
 |-  ( ph -> N e. Fin )
7 mamufval.p 
 |-  ( ph -> P e. Fin )
8 df-mamu 
 |-  maMul = ( r e. _V , o e. _V |-> [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )
9 8 a1i 
 |-  ( ph -> maMul = ( r e. _V , o e. _V |-> [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) ) )
10 fvex 
 |-  ( 1st ` ( 1st ` o ) ) e. _V
11 fvex 
 |-  ( 2nd ` ( 1st ` o ) ) e. _V
12 fvex 
 |-  ( 2nd ` o ) e. _V
13 eqidd 
 |-  ( p = ( 2nd ` o ) -> ( ( Base ` r ) ^m ( m X. n ) ) = ( ( Base ` r ) ^m ( m X. n ) ) )
14 xpeq2 
 |-  ( p = ( 2nd ` o ) -> ( n X. p ) = ( n X. ( 2nd ` o ) ) )
15 14 oveq2d 
 |-  ( p = ( 2nd ` o ) -> ( ( Base ` r ) ^m ( n X. p ) ) = ( ( Base ` r ) ^m ( n X. ( 2nd ` o ) ) ) )
16 eqidd 
 |-  ( p = ( 2nd ` o ) -> m = m )
17 id 
 |-  ( p = ( 2nd ` o ) -> p = ( 2nd ` o ) )
18 eqidd 
 |-  ( p = ( 2nd ` o ) -> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) = ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) )
19 16 17 18 mpoeq123dv 
 |-  ( p = ( 2nd ` o ) -> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) = ( i e. m , k e. ( 2nd ` o ) |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
20 13 15 19 mpoeq123dv 
 |-  ( p = ( 2nd ` o ) -> ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) = ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. ( 2nd ` o ) ) ) |-> ( i e. m , k e. ( 2nd ` o ) |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )
21 12 20 csbie 
 |-  [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) = ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. ( 2nd ` o ) ) ) |-> ( i e. m , k e. ( 2nd ` o ) |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
22 xpeq12 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( m X. n ) = ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) )
23 22 oveq2d 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( ( Base ` r ) ^m ( m X. n ) ) = ( ( Base ` r ) ^m ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) ) )
24 simpr 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> n = ( 2nd ` ( 1st ` o ) ) )
25 24 xpeq1d 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( n X. ( 2nd ` o ) ) = ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) )
26 25 oveq2d 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( ( Base ` r ) ^m ( n X. ( 2nd ` o ) ) ) = ( ( Base ` r ) ^m ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) ) )
27 id 
 |-  ( m = ( 1st ` ( 1st ` o ) ) -> m = ( 1st ` ( 1st ` o ) ) )
28 27 adantr 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> m = ( 1st ` ( 1st ` o ) ) )
29 eqidd 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( 2nd ` o ) = ( 2nd ` o ) )
30 eqidd 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( ( i x j ) ( .r ` r ) ( j y k ) ) = ( ( i x j ) ( .r ` r ) ( j y k ) ) )
31 24 30 mpteq12dv 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) = ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) )
32 31 oveq2d 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) = ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) )
33 28 29 32 mpoeq123dv 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( i e. m , k e. ( 2nd ` o ) |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) = ( i e. ( 1st ` ( 1st ` o ) ) , k e. ( 2nd ` o ) |-> ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
34 23 26 33 mpoeq123dv 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. ( 2nd ` o ) ) ) |-> ( i e. m , k e. ( 2nd ` o ) |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) = ( x e. ( ( Base ` r ) ^m ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) ) , y e. ( ( Base ` r ) ^m ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) ) |-> ( i e. ( 1st ` ( 1st ` o ) ) , k e. ( 2nd ` o ) |-> ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )
35 21 34 syl5eq 
 |-  ( ( m = ( 1st ` ( 1st ` o ) ) /\ n = ( 2nd ` ( 1st ` o ) ) ) -> [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) = ( x e. ( ( Base ` r ) ^m ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) ) , y e. ( ( Base ` r ) ^m ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) ) |-> ( i e. ( 1st ` ( 1st ` o ) ) , k e. ( 2nd ` o ) |-> ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )
36 10 11 35 csbie2 
 |-  [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) = ( x e. ( ( Base ` r ) ^m ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) ) , y e. ( ( Base ` r ) ^m ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) ) |-> ( i e. ( 1st ` ( 1st ` o ) ) , k e. ( 2nd ` o ) |-> ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
37 simprl 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> r = R )
38 37 fveq2d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( Base ` r ) = ( Base ` R ) )
39 38 2 eqtr4di 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( Base ` r ) = B )
40 fveq2 
 |-  ( o = <. M , N , P >. -> ( 1st ` o ) = ( 1st ` <. M , N , P >. ) )
41 40 fveq2d 
 |-  ( o = <. M , N , P >. -> ( 1st ` ( 1st ` o ) ) = ( 1st ` ( 1st ` <. M , N , P >. ) ) )
42 41 ad2antll 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 1st ` ( 1st ` o ) ) = ( 1st ` ( 1st ` <. M , N , P >. ) ) )
43 ot1stg 
 |-  ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> ( 1st ` ( 1st ` <. M , N , P >. ) ) = M )
44 5 6 7 43 syl3anc 
 |-  ( ph -> ( 1st ` ( 1st ` <. M , N , P >. ) ) = M )
45 44 adantr 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 1st ` ( 1st ` <. M , N , P >. ) ) = M )
46 42 45 eqtrd 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 1st ` ( 1st ` o ) ) = M )
47 40 fveq2d 
 |-  ( o = <. M , N , P >. -> ( 2nd ` ( 1st ` o ) ) = ( 2nd ` ( 1st ` <. M , N , P >. ) ) )
48 47 ad2antll 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 2nd ` ( 1st ` o ) ) = ( 2nd ` ( 1st ` <. M , N , P >. ) ) )
49 ot2ndg 
 |-  ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> ( 2nd ` ( 1st ` <. M , N , P >. ) ) = N )
50 5 6 7 49 syl3anc 
 |-  ( ph -> ( 2nd ` ( 1st ` <. M , N , P >. ) ) = N )
51 50 adantr 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 2nd ` ( 1st ` <. M , N , P >. ) ) = N )
52 48 51 eqtrd 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 2nd ` ( 1st ` o ) ) = N )
53 46 52 xpeq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) = ( M X. N ) )
54 39 53 oveq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( ( Base ` r ) ^m ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) ) = ( B ^m ( M X. N ) ) )
55 fveq2 
 |-  ( o = <. M , N , P >. -> ( 2nd ` o ) = ( 2nd ` <. M , N , P >. ) )
56 55 ad2antll 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 2nd ` o ) = ( 2nd ` <. M , N , P >. ) )
57 ot3rdg 
 |-  ( P e. Fin -> ( 2nd ` <. M , N , P >. ) = P )
58 7 57 syl 
 |-  ( ph -> ( 2nd ` <. M , N , P >. ) = P )
59 58 adantr 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 2nd ` <. M , N , P >. ) = P )
60 56 59 eqtrd 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( 2nd ` o ) = P )
61 52 60 xpeq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) = ( N X. P ) )
62 39 61 oveq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( ( Base ` r ) ^m ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) ) = ( B ^m ( N X. P ) ) )
63 37 fveq2d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( .r ` r ) = ( .r ` R ) )
64 63 3 eqtr4di 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( .r ` r ) = .x. )
65 64 oveqd 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( ( i x j ) ( .r ` r ) ( j y k ) ) = ( ( i x j ) .x. ( j y k ) ) )
66 52 65 mpteq12dv 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) = ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) )
67 37 66 oveq12d 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) = ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) )
68 46 60 67 mpoeq123dv 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( i e. ( 1st ` ( 1st ` o ) ) , k e. ( 2nd ` o ) |-> ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) = ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) )
69 54 62 68 mpoeq123dv 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> ( x e. ( ( Base ` r ) ^m ( ( 1st ` ( 1st ` o ) ) X. ( 2nd ` ( 1st ` o ) ) ) ) , y e. ( ( Base ` r ) ^m ( ( 2nd ` ( 1st ` o ) ) X. ( 2nd ` o ) ) ) |-> ( i e. ( 1st ` ( 1st ` o ) ) , k e. ( 2nd ` o ) |-> ( r gsum ( j e. ( 2nd ` ( 1st ` o ) ) |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) )
70 36 69 syl5eq 
 |-  ( ( ph /\ ( r = R /\ o = <. M , N , P >. ) ) -> [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) )
71 4 elexd 
 |-  ( ph -> R e. _V )
72 otex 
 |-  <. M , N , P >. e. _V
73 72 a1i 
 |-  ( ph -> <. M , N , P >. e. _V )
74 ovex 
 |-  ( B ^m ( M X. N ) ) e. _V
75 ovex 
 |-  ( B ^m ( N X. P ) ) e. _V
76 74 75 mpoex 
 |-  ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) e. _V
77 76 a1i 
 |-  ( ph -> ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) e. _V )
78 9 70 71 73 77 ovmpod 
 |-  ( ph -> ( R maMul <. M , N , P >. ) = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) )
79 1 78 syl5eq 
 |-  ( ph -> F = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) .x. ( j y k ) ) ) ) ) ) )