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

Theorem mamufval 19410
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 19409 . . . 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 5875 . . . . 5  |-  ( 1st `  ( 1st `  o
) )  e.  _V
5 fvex 5875 . . . . 5  |-  ( 2nd `  ( 1st `  o
) )  e.  _V
6 fvex 5875 . . . . . . 7  |-  ( 2nd `  o )  e.  _V
7 eqidd 2452 . . . . . . . 8  |-  ( p  =  ( 2nd `  o
)  ->  ( ( Base `  r )  ^m  ( m  X.  n
) )  =  ( ( Base `  r
)  ^m  ( m  X.  n ) ) )
8 xpeq2 4849 . . . . . . . . 9  |-  ( p  =  ( 2nd `  o
)  ->  ( n  X.  p )  =  ( n  X.  ( 2nd `  o ) ) )
98oveq2d 6306 . . . . . . . 8  |-  ( p  =  ( 2nd `  o
)  ->  ( ( Base `  r )  ^m  ( n  X.  p
) )  =  ( ( Base `  r
)  ^m  ( n  X.  ( 2nd `  o
) ) ) )
10 eqidd 2452 . . . . . . . . 9  |-  ( p  =  ( 2nd `  o
)  ->  m  =  m )
11 id 22 . . . . . . . . 9  |-  ( p  =  ( 2nd `  o
)  ->  p  =  ( 2nd `  o ) )
12 eqidd 2452 . . . . . . . . 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 6353 . . . . . . . 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 6353 . . . . . . 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 3389 . . . . . 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 4853 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( m  X.  n )  =  ( ( 1st `  ( 1st `  o ) )  X.  ( 2nd `  ( 1st `  o ) ) ) )
1716oveq2d 6306 . . . . . . 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 463 . . . . . . . . 9  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  n  =  ( 2nd `  ( 1st `  o ) ) )
1918xpeq1d 4857 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( n  X.  ( 2nd `  o
) )  =  ( ( 2nd `  ( 1st `  o ) )  X.  ( 2nd `  o
) ) )
2019oveq2d 6306 . . . . . . 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 467 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  m  =  ( 1st `  ( 1st `  o ) ) )
23 eqidd 2452 . . . . . . . 8  |-  ( ( m  =  ( 1st `  ( 1st `  o
) )  /\  n  =  ( 2nd `  ( 1st `  o ) ) )  ->  ( 2nd `  o )  =  ( 2nd `  o ) )
24 eqidd 2452 . . . . . . . . . 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 4481 . . . . . . . . 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 6306 . . . . . . . 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 6353 . . . . . . 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 6353 . . . . . 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 2497 . . . . 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 3393 . . . 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 764 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
r  =  R )
3231fveq2d 5869 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( Base `  r )  =  ( Base `  R
) )
33 mamufval.b . . . . . . 7  |-  B  =  ( Base `  R
)
3432, 33syl6eqr 2503 . . . . . 6  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( Base `  r )  =  B )
35 fveq2 5865 . . . . . . . . . 10  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 1st `  o )  =  ( 1st `  <. M ,  N ,  P >. ) )
3635fveq2d 5869 . . . . . . . . 9  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 1st `  ( 1st `  o
) )  =  ( 1st `  ( 1st `  <. M ,  N ,  P >. ) ) )
3736ad2antll 735 . . . . . . . 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 6807 . . . . . . . . . 10  |-  ( ( M  e.  Fin  /\  N  e.  Fin  /\  P  e.  Fin )  ->  ( 1st `  ( 1st `  <. M ,  N ,  P >. ) )  =  M )
4238, 39, 40, 41syl3anc 1268 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  ( 1st `  <. M ,  N ,  P >. ) )  =  M )
4342adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 1st `  ( 1st `  <. M ,  N ,  P >. ) )  =  M )
4437, 43eqtrd 2485 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 1st `  ( 1st `  o ) )  =  M )
4535fveq2d 5869 . . . . . . . . 9  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 2nd `  ( 1st `  o
) )  =  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) ) )
4645ad2antll 735 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  ( 1st `  o ) )  =  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) ) )
47 ot2ndg 6808 . . . . . . . . . 10  |-  ( ( M  e.  Fin  /\  N  e.  Fin  /\  P  e.  Fin )  ->  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) )  =  N )
4838, 39, 40, 47syl3anc 1268 . . . . . . . . 9  |-  ( ph  ->  ( 2nd `  ( 1st `  <. M ,  N ,  P >. ) )  =  N )
4948adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  ( 1st `  <. M ,  N ,  P >. ) )  =  N )
5046, 49eqtrd 2485 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  ( 1st `  o ) )  =  N )
5144, 50xpeq12d 4859 . . . . . 6  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( 1st `  ( 1st `  o ) )  X.  ( 2nd `  ( 1st `  o ) ) )  =  ( M  X.  N ) )
5234, 51oveq12d 6308 . . . . 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 5865 . . . . . . . . 9  |-  ( o  =  <. M ,  N ,  P >.  ->  ( 2nd `  o )  =  ( 2nd `  <. M ,  N ,  P >. ) )
5453ad2antll 735 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  o
)  =  ( 2nd `  <. M ,  N ,  P >. ) )
55 ot3rdg 6809 . . . . . . . . . 10  |-  ( P  e.  Fin  ->  ( 2nd `  <. M ,  N ,  P >. )  =  P )
5640, 55syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 2nd `  <. M ,  N ,  P >. )  =  P )
5756adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  <. M ,  N ,  P >. )  =  P )
5854, 57eqtrd 2485 . . . . . . 7  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( 2nd `  o
)  =  P )
5950, 58xpeq12d 4859 . . . . . 6  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( 2nd `  ( 1st `  o ) )  X.  ( 2nd `  o
) )  =  ( N  X.  P ) )
6034, 59oveq12d 6308 . . . . 5  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( ( Base `  r
)  ^m  ( ( 2nd `  ( 1st `  o
) )  X.  ( 2nd `  o ) ) )  =  ( B  ^m  ( N  X.  P ) ) )
6131fveq2d 5869 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( .r `  r
)  =  ( .r
`  R ) )
62 mamufval.t . . . . . . . . . 10  |-  .x.  =  ( .r `  R )
6361, 62syl6eqr 2503 . . . . . . . . 9  |-  ( (
ph  /\  ( r  =  R  /\  o  =  <. M ,  N ,  P >. ) )  -> 
( .r `  r
)  =  .x.  )
6463oveqd 6307 . . . . . . . 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 4481 . . . . . . 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 6308 . . . . . 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 6353 . . . . 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 6353 . . . 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 2497 . . 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 3054 . . . 4  |-  ( R  e.  V  ->  R  e.  _V )
7270, 71syl 17 . . 3  |-  ( ph  ->  R  e.  _V )
73 otex 4665 . . . 4  |-  <. M ,  N ,  P >.  e. 
_V
7473a1i 11 . . 3  |-  ( ph  -> 
<. M ,  N ,  P >.  e.  _V )
75 ovex 6318 . . . . 5  |-  ( B  ^m  ( M  X.  N ) )  e. 
_V
76 ovex 6318 . . . . 5  |-  ( B  ^m  ( N  X.  P ) )  e. 
_V
7775, 76mpt2ex 6870 . . . 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 6424 . 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 2497 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 371    = wceq 1444    e. wcel 1887   _Vcvv 3045   [_csb 3363   <.cotp 3976    |-> cmpt 4461    X. cxp 4832   ` cfv 5582  (class class class)co 6290    |-> cmpt2 6292   1stc1st 6791   2ndc2nd 6792    ^m cmap 7472   Fincfn 7569   Basecbs 15121   .rcmulr 15191    gsumg cgsu 15339   maMul cmmul 19408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-ot 3977  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-mamu 19409
This theorem is referenced by:  mamuval  19411  mamudm  19413
  Copyright terms: Public domain W3C validator