MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mamufval Structured version   Unicode version

Theorem mamufval 19069
Description: Functional value of the matrix multiplication operator. (Contributed by Stefan O'Rear, 2-Sep-2015.)
Hypotheses
Ref Expression
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
Ref Expression
mamufval  |-  ( ph  ->  F  =  ( x  e.  ( B  ^m  ( M  X.  N
) ) ,  y  e.  ( B  ^m  ( N  X.  P
) )  |->  ( i  e.  M ,  k  e.  P  |->  ( R 
gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) ) )
Distinct variable groups:    i, j,
k, x, y, M   
i, N, j, k, x, y    P, i, j, k, x, y    R, i, j, k, x, y    ph, i, j, k, x, y    x, B, y    x,  .x. , y, i, k
Allowed substitution hints:    B( i, j, k)    .x. ( j)    F( x, y, i, j, k)    V( x, y, i, j, k)

Proof of Theorem mamufval
Dummy variables  m  n  o  p  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mamufval.f . 2  |-  F  =  ( R maMul  <. M ,  N ,  P >. )
2 df-mamu 19068 . . . 4  |- 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  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) ) ) ) ) )
32a1i 11 . . 3  |-  ( 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  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) ) ) ) ) ) )
4 fvex 5813 . . . . 5  |-  ( 1st `  ( 1st `  o
) )  e.  _V
5 fvex 5813 . . . . 5  |-  ( 2nd `  ( 1st `  o
) )  e.  _V
6 fvex 5813 . . . . . . 7  |-  ( 2nd `  o )  e.  _V
7 eqidd 2401 . . . . . . . 8  |-  ( p  =  ( 2nd `  o
)  ->  ( ( Base `  r )  ^m  ( m  X.  n
) )  =  ( ( Base `  r
)  ^m  ( m  X.  n ) ) )
8 xpeq2 4955 . . . . . . . . 9  |-  ( p  =  ( 2nd `  o
)  ->  ( n  X.  p )  =  ( n  X.  ( 2nd `  o ) ) )
98oveq2d 6248 . . . . . . . 8  |-  ( p  =  ( 2nd `  o
)  ->  ( ( Base `  r )  ^m  ( n  X.  p
) )  =  ( ( Base `  r
)  ^m  ( n  X.  ( 2nd `  o
) ) ) )
10 eqidd 2401 . . . . . . . . 9  |-  ( p  =  ( 2nd `  o
)  ->  m  =  m )
11 id 22 . . . . . . . . 9  |-  ( p  =  ( 2nd `  o
)  ->  p  =  ( 2nd `  o ) )
12 eqidd 2401 . . . . . . . . 9  |-  ( p  =  ( 2nd `  o
)  ->  ( r  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r `  r ) ( j y k ) ) ) )  =  ( r  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) )
1310, 11, 12mpt2eq123dv 6294 . . . . . . . 8  |-  ( p  =  ( 2nd `  o
)  ->  ( i  e.  m ,  k  e.  p  |->  ( r  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) ) ) )  =  ( i  e.  m ,  k  e.  ( 2nd `  o )  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) ) )
147, 9, 13mpt2eq123dv 6294 . . . . . . 7  |-  ( 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 
gsumg  ( 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 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) ) ) )
156, 14csbie 3396 . . . . . 6  |-  [_ ( 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 
gsumg  ( 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 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) ) )
16 xpeq12 4959 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( m  X.  n )  =  ( ( 1st `  ( 1st `  o ) )  X.  ( 2nd `  ( 1st `  o ) ) ) )
1716oveq2d 6248 . . . . . . 7  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( ( Base `  r )  ^m  ( m  X.  n
) )  =  ( ( Base `  r
)  ^m  ( ( 1st `  ( 1st `  o
) )  X.  ( 2nd `  ( 1st `  o
) ) ) ) )
18 simpr 459 . . . . . . . . 9  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  n  =  ( 2nd `  ( 1st `  o ) ) )
1918xpeq1d 4963 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( n  X.  ( 2nd `  o
) )  =  ( ( 2nd `  ( 1st `  o ) )  X.  ( 2nd `  o
) ) )
2019oveq2d 6248 . . . . . . 7  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( ( Base `  r )  ^m  ( n  X.  ( 2nd `  o ) ) )  =  ( (
Base `  r )  ^m  ( ( 2nd `  ( 1st `  o ) )  X.  ( 2nd `  o
) ) ) )
21 id 22 . . . . . . . . 9  |-  ( m  =  ( 1st `  ( 1st `  o ) )  ->  m  =  ( 1st `  ( 1st `  o ) ) )
2221adantr 463 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  m  =  ( 1st `  ( 1st `  o ) ) )
23 eqidd 2401 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( 2nd `  o )  =  ( 2nd `  o ) )
24 eqidd 2401 . . . . . . . . . 10  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( (
i x j ) ( .r `  r
) ( j y k ) )  =  ( ( i x j ) ( .r
`  r ) ( j y k ) ) )
2518, 24mpteq12dv 4470 . . . . . . . . 9  |-  ( ( 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 ) ) ) )
2625oveq2d 6248 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( r  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r `  r ) ( j y k ) ) ) )  =  ( r  gsumg  ( j  e.  ( 2nd `  ( 1st `  o ) )  |->  ( ( i x j ) ( .r `  r ) ( j y k ) ) ) ) )
2722, 23, 26mpt2eq123dv 6294 . . . . . . 7  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( i  e.  m ,  k  e.  ( 2nd `  o
)  |->  ( r  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) ) ) )  =  ( i  e.  ( 1st `  ( 1st `  o
) ) ,  k  e.  ( 2nd `  o
)  |->  ( r  gsumg  ( j  e.  ( 2nd `  ( 1st `  o ) ) 
|->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) ) )
2817, 20, 27mpt2eq123dv 6294 . . . . . 6  |-  ( ( 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  gsumg  ( 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  gsumg  ( j  e.  ( 2nd `  ( 1st `  o ) )  |->  ( ( i x j ) ( .r `  r ) ( j y k ) ) ) ) ) ) )
2915, 28syl5eq 2453 . . . . 5  |-  ( ( 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 
gsumg  ( 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  gsumg  ( j  e.  ( 2nd `  ( 1st `  o ) ) 
|->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) ) ) )
304, 5, 29csbie2 3400 . . . 4  |-  [_ ( 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 
gsumg  ( 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  gsumg  ( j  e.  ( 2nd `  ( 1st `  o ) ) 
|->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) ) )
31 simprl 755 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
r  =  R )
3231fveq2d 5807 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( Base `  r )  =  ( Base `  R
) )
33 mamufval.b . . . . . . 7  |-  B  =  ( Base `  R
)
3432, 33syl6eqr 2459 . . . . . 6  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( Base `  r )  =  B )
35 fveq2 5803 . . . . . . . . . 10  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 1st `  o )  =  ( 1st `  <. M ,  N ,  P >. ) )
3635fveq2d 5807 . . . . . . . . 9  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 1st `  ( 1st `  o
) )  =  ( 1st `  ( 1st `  <. M ,  N ,  P >. ) ) )
3736ad2antll 727 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 1st `  ( 1st `  o ) )  =  ( 1st `  ( 1st `  <. M ,  N ,  P >. ) ) )
38 mamufval.m . . . . . . . . . 10  |-  ( ph  ->  M  e.  Fin )
39 mamufval.n . . . . . . . . . 10  |-  ( ph  ->  N  e.  Fin )
40 mamufval.p . . . . . . . . . 10  |-  ( ph  ->  P  e.  Fin )
41 ot1stg 6750 . . . . . . . . . 10  |-  ( ( M  e.  Fin  /\  N  e.  Fin  /\  P  e.  Fin )  ->  ( 1st `  ( 1st `  <. M ,  N ,  P >. ) )  =  M )
4238, 39, 40, 41syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  ( 1st `  <. M ,  N ,  P >. ) )  =  M )
4342adantr 463 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 1st `  ( 1st `  <. M ,  N ,  P >. ) )  =  M )
4437, 43eqtrd 2441 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 1st `  ( 1st `  o ) )  =  M )
4535fveq2d 5807 . . . . . . . . 9  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 2nd `  ( 1st `  o
) )  =  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) ) )
4645ad2antll 727 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  ( 1st `  o ) )  =  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) ) )
47 ot2ndg 6751 . . . . . . . . . 10  |-  ( ( M  e.  Fin  /\  N  e.  Fin  /\  P  e.  Fin )  ->  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) )  =  N )
4838, 39, 40, 47syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) )  =  N )
4948adantr 463 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  ( 1st `  <. M ,  N ,  P >. ) )  =  N )
5046, 49eqtrd 2441 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  ( 1st `  o ) )  =  N )
5144, 50xpeq12d 4965 . . . . . 6  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( 1st `  ( 1st `  o ) )  X.  ( 2nd `  ( 1st `  o ) ) )  =  ( M  X.  N ) )
5234, 51oveq12d 6250 . . . . 5  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( Base `  r
)  ^m  ( ( 1st `  ( 1st `  o
) )  X.  ( 2nd `  ( 1st `  o
) ) ) )  =  ( B  ^m  ( M  X.  N
) ) )
53 fveq2 5803 . . . . . . . . 9  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 2nd `  o )  =  ( 2nd `  <. M ,  N ,  P >. ) )
5453ad2antll 727 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  o
)  =  ( 2nd `  <. M ,  N ,  P >. ) )
55 ot3rdg 6752 . . . . . . . . . 10  |-  ( P  e.  Fin  ->  ( 2nd `  <. M ,  N ,  P >. )  =  P )
5640, 55syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 2nd `  <. M ,  N ,  P >. )  =  P )
5756adantr 463 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  <. M ,  N ,  P >. )  =  P )
5854, 57eqtrd 2441 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  o
)  =  P )
5950, 58xpeq12d 4965 . . . . . 6  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( 2nd `  ( 1st `  o ) )  X.  ( 2nd `  o
) )  =  ( N  X.  P ) )
6034, 59oveq12d 6250 . . . . 5  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( Base `  r
)  ^m  ( ( 2nd `  ( 1st `  o
) )  X.  ( 2nd `  o ) ) )  =  ( B  ^m  ( N  X.  P ) ) )
6131fveq2d 5807 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( .r `  r
)  =  ( .r
`  R ) )
62 mamufval.t . . . . . . . . . 10  |-  .x.  =  ( .r `  R )
6361, 62syl6eqr 2459 . . . . . . . . 9  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( .r `  r
)  =  .x.  )
6463oveqd 6249 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( i x j ) ( .r
`  r ) ( j y k ) )  =  ( ( i x j ) 
.x.  ( j y k ) ) )
6550, 64mpteq12dv 4470 . . . . . . 7  |-  ( (
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 ) ) ) )
6631, 65oveq12d 6250 . . . . . 6  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( r  gsumg  ( j  e.  ( 2nd `  ( 1st `  o ) )  |->  ( ( i x j ) ( .r `  r ) ( j y k ) ) ) )  =  ( R  gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) )
6744, 58, 66mpt2eq123dv 6294 . . . . 5  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( i  e.  ( 1st `  ( 1st `  o ) ) ,  k  e.  ( 2nd `  o )  |->  ( r 
gsumg  ( j  e.  ( 2nd `  ( 1st `  o ) )  |->  ( ( i x j ) ( .r `  r ) ( j y k ) ) ) ) )  =  ( i  e.  M ,  k  e.  P  |->  ( R  gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) )
6852, 60, 67mpt2eq123dv 6294 . . . 4  |-  ( (
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  gsumg  ( 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  gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) ) )
6930, 68syl5eq 2453 . . 3  |-  ( (
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  gsumg  ( 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  gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) ) )
70 mamufval.r . . . 4  |-  ( ph  ->  R  e.  V )
71 elex 3065 . . . 4  |-  ( R  e.  V  ->  R  e.  _V )
7270, 71syl 17 . . 3  |-  ( ph  ->  R  e.  _V )
73 otex 4653 . . . 4  |-  <. M ,  N ,  P >.  e. 
_V
7473a1i 11 . . 3  |-  ( ph  -> 
<. M ,  N ,  P >.  e.  _V )
75 ovex 6260 . . . . 5  |-  ( B  ^m  ( M  X.  N ) )  e. 
_V
76 ovex 6260 . . . . 5  |-  ( B  ^m  ( N  X.  P ) )  e. 
_V
7775, 76mpt2ex 6813 . . . 4  |-  ( x  e.  ( B  ^m  ( M  X.  N
) ) ,  y  e.  ( B  ^m  ( N  X.  P
) )  |->  ( i  e.  M ,  k  e.  P  |->  ( R 
gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) )  e.  _V
7877a1i 11 . . 3  |-  ( ph  ->  ( x  e.  ( B  ^m  ( M  X.  N ) ) ,  y  e.  ( B  ^m  ( N  X.  P ) ) 
|->  ( i  e.  M ,  k  e.  P  |->  ( R  gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) )  e.  _V )
793, 69, 72, 74, 78ovmpt2d 6365 . 2  |-  ( 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  gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) ) )
801, 79syl5eq 2453 1  |-  ( ph  ->  F  =  ( x  e.  ( B  ^m  ( M  X.  N
) ) ,  y  e.  ( B  ^m  ( N  X.  P
) )  |->  ( i  e.  M ,  k  e.  P  |->  ( R 
gsumg  ( j  e.  N  |->  ( ( i x j )  .x.  (
j y k ) ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1403    e. wcel 1840   _Vcvv 3056   [_csb 3370   <.cotp 3977    |-> cmpt 4450    X. cxp 4938   ` cfv 5523  (class class class)co 6232    |-> cmpt2 6234   1stc1st 6734   2ndc2nd 6735    ^m cmap 7375   Fincfn 7472   Basecbs 14731   .rcmulr 14800    gsumg cgsu 14945   maMul cmmul 19067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-8 1842  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4569  ax-pr 4627  ax-un 6528
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rex 2757  df-reu 2758  df-rab 2760  df-v 3058  df-sbc 3275  df-csb 3371  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-op 3976  df-ot 3978  df-uni 4189  df-iun 4270  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4735  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5487  df-fun 5525  df-fn 5526  df-f 5527  df-f1 5528  df-fo 5529  df-f1o 5530  df-fv 5531  df-ov 6235  df-oprab 6236  df-mpt2 6237  df-1st 6736  df-2nd 6737  df-mamu 19068
This theorem is referenced by:  mamuval  19070  mamudm  19072
  Copyright terms: Public domain W3C validator