Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mamu Unicode version

Definition df-mamu 27313
Description: The operator which multiplies an MxN matrix with an NxP matrix. Note that it is not generally possible to recover the dimensions from the matrix, since all Nx0 and all 0xN matrices are represented by the empty set. (Contributed by Stefan O'Rear, 4-Sep-2015.)
Assertion
Ref Expression
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  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) ) ) ) ) )
Distinct variable group:    i, j, k, m, n, o, p, r, x, y

Detailed syntax breakdown of Definition df-mamu
StepHypRef Expression
1 cmmul 27311 . 2  class maMul
2 vr . . 3  set  r
3 vo . . 3  set  o
4 cvv 2920 . . 3  class  _V
5 vm . . . 4  set  m
63cv 1648 . . . . . 6  class  o
7 c1st 6310 . . . . . 6  class  1st
86, 7cfv 5417 . . . . 5  class  ( 1st `  o )
98, 7cfv 5417 . . . 4  class  ( 1st `  ( 1st `  o
) )
10 vn . . . . 5  set  n
11 c2nd 6311 . . . . . 6  class  2nd
128, 11cfv 5417 . . . . 5  class  ( 2nd `  ( 1st `  o
) )
13 vp . . . . . 6  set  p
146, 11cfv 5417 . . . . . 6  class  ( 2nd `  o )
15 vx . . . . . . 7  set  x
16 vy . . . . . . 7  set  y
172cv 1648 . . . . . . . . 9  class  r
18 cbs 13428 . . . . . . . . 9  class  Base
1917, 18cfv 5417 . . . . . . . 8  class  ( Base `  r )
205cv 1648 . . . . . . . . 9  class  m
2110cv 1648 . . . . . . . . 9  class  n
2220, 21cxp 4839 . . . . . . . 8  class  ( m  X.  n )
23 cmap 6981 . . . . . . . 8  class  ^m
2419, 22, 23co 6044 . . . . . . 7  class  ( (
Base `  r )  ^m  ( m  X.  n
) )
2513cv 1648 . . . . . . . . 9  class  p
2621, 25cxp 4839 . . . . . . . 8  class  ( n  X.  p )
2719, 26, 23co 6044 . . . . . . 7  class  ( (
Base `  r )  ^m  ( n  X.  p
) )
28 vi . . . . . . . 8  set  i
29 vk . . . . . . . 8  set  k
30 vj . . . . . . . . . 10  set  j
3128cv 1648 . . . . . . . . . . . 12  class  i
3230cv 1648 . . . . . . . . . . . 12  class  j
3315cv 1648 . . . . . . . . . . . 12  class  x
3431, 32, 33co 6044 . . . . . . . . . . 11  class  ( i x j )
3529cv 1648 . . . . . . . . . . . 12  class  k
3616cv 1648 . . . . . . . . . . . 12  class  y
3732, 35, 36co 6044 . . . . . . . . . . 11  class  ( j y k )
38 cmulr 13489 . . . . . . . . . . . 12  class  .r
3917, 38cfv 5417 . . . . . . . . . . 11  class  ( .r
`  r )
4034, 37, 39co 6044 . . . . . . . . . 10  class  ( ( i x j ) ( .r `  r
) ( j y k ) )
4130, 21, 40cmpt 4230 . . . . . . . . 9  class  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) )
42 cgsu 13683 . . . . . . . . 9  class  gsumg
4317, 41, 42co 6044 . . . . . . . 8  class  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) )
4428, 29, 20, 25, 43cmpt2 6046 . . . . . . 7  class  ( i  e.  m ,  k  e.  p  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) ) )
4515, 16, 24, 27, 44cmpt2 6046 . . . . . 6  class  ( 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 ) ) ) ) ) )
4613, 14, 45csb 3215 . . . . 5  class  [_ ( 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 ) ) ) ) ) )
4710, 12, 46csb 3215 . . . 4  class  [_ ( 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 ) ) ) ) ) )
485, 9, 47csb 3215 . . 3  class  [_ ( 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 ) ) ) ) ) )
492, 3, 4, 4, 48cmpt2 6046 . 2  class  ( 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 ) ) ) ) ) ) )
501, 49wceq 1649 1  wff 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 ) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  mamufval  27315
  Copyright terms: Public domain W3C validator