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 26764
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 26762 . 2  class maMul
2 vr . . 3  set  r
3 vo . . 3  set  o
4 cvv 2864 . . 3  class  _V
5 vm . . . 4  set  m
63cv 1641 . . . . . 6  class  o
7 c1st 6207 . . . . . 6  class  1st
86, 7cfv 5337 . . . . 5  class  ( 1st `  o )
98, 7cfv 5337 . . . 4  class  ( 1st `  ( 1st `  o
) )
10 vn . . . . 5  set  n
11 c2nd 6208 . . . . . 6  class  2nd
128, 11cfv 5337 . . . . 5  class  ( 2nd `  ( 1st `  o
) )
13 vp . . . . . 6  set  p
146, 11cfv 5337 . . . . . 6  class  ( 2nd `  o )
15 vx . . . . . . 7  set  x
16 vy . . . . . . 7  set  y
172cv 1641 . . . . . . . . 9  class  r
18 cbs 13245 . . . . . . . . 9  class  Base
1917, 18cfv 5337 . . . . . . . 8  class  ( Base `  r )
205cv 1641 . . . . . . . . 9  class  m
2110cv 1641 . . . . . . . . 9  class  n
2220, 21cxp 4769 . . . . . . . 8  class  ( m  X.  n )
23 cmap 6860 . . . . . . . 8  class  ^m
2419, 22, 23co 5945 . . . . . . 7  class  ( (
Base `  r )  ^m  ( m  X.  n
) )
2513cv 1641 . . . . . . . . 9  class  p
2621, 25cxp 4769 . . . . . . . 8  class  ( n  X.  p )
2719, 26, 23co 5945 . . . . . . 7  class  ( (
Base `  r )  ^m  ( n  X.  p
) )
28 vi . . . . . . . 8  set  i
29 vk . . . . . . . 8  set  k
30 vj . . . . . . . . . 10  set  j
3128cv 1641 . . . . . . . . . . . 12  class  i
3230cv 1641 . . . . . . . . . . . 12  class  j
3315cv 1641 . . . . . . . . . . . 12  class  x
3431, 32, 33co 5945 . . . . . . . . . . 11  class  ( i x j )
3529cv 1641 . . . . . . . . . . . 12  class  k
3616cv 1641 . . . . . . . . . . . 12  class  y
3732, 35, 36co 5945 . . . . . . . . . . 11  class  ( j y k )
38 cmulr 13306 . . . . . . . . . . . 12  class  .r
3917, 38cfv 5337 . . . . . . . . . . 11  class  ( .r
`  r )
4034, 37, 39co 5945 . . . . . . . . . 10  class  ( ( i x j ) ( .r `  r
) ( j y k ) )
4130, 21, 40cmpt 4158 . . . . . . . . 9  class  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) )
42 cgsu 13500 . . . . . . . . 9  class  gsumg
4317, 41, 42co 5945 . . . . . . . 8  class  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) )
4428, 29, 20, 25, 43cmpt2 5947 . . . . . . 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 5947 . . . . . 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 3157 . . . . 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 3157 . . . 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 3157 . . 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 5947 . 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 1642 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  26766
  Copyright terms: Public domain W3C validator