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 27441
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 27439 . 2  class maMul
2 vr . . 3  set  r
3 vo . . 3  set  o
4 cvv 2788 . . 3  class  _V
5 vm . . . 4  set  m
63cv 1622 . . . . . 6  class  o
7 c1st 6120 . . . . . 6  class  1st
86, 7cfv 5255 . . . . 5  class  ( 1st `  o )
98, 7cfv 5255 . . . 4  class  ( 1st `  ( 1st `  o
) )
10 vn . . . . 5  set  n
11 c2nd 6121 . . . . . 6  class  2nd
128, 11cfv 5255 . . . . 5  class  ( 2nd `  ( 1st `  o
) )
13 vp . . . . . 6  set  p
146, 11cfv 5255 . . . . . 6  class  ( 2nd `  o )
15 vx . . . . . . 7  set  x
16 vy . . . . . . 7  set  y
172cv 1622 . . . . . . . . 9  class  r
18 cbs 13148 . . . . . . . . 9  class  Base
1917, 18cfv 5255 . . . . . . . 8  class  ( Base `  r )
205cv 1622 . . . . . . . . 9  class  m
2110cv 1622 . . . . . . . . 9  class  n
2220, 21cxp 4687 . . . . . . . 8  class  ( m  X.  n )
23 cmap 6772 . . . . . . . 8  class  ^m
2419, 22, 23co 5858 . . . . . . 7  class  ( (
Base `  r )  ^m  ( m  X.  n
) )
2513cv 1622 . . . . . . . . 9  class  p
2621, 25cxp 4687 . . . . . . . 8  class  ( n  X.  p )
2719, 26, 23co 5858 . . . . . . 7  class  ( (
Base `  r )  ^m  ( n  X.  p
) )
28 vi . . . . . . . 8  set  i
29 vk . . . . . . . 8  set  k
30 vj . . . . . . . . . 10  set  j
3128cv 1622 . . . . . . . . . . . 12  class  i
3230cv 1622 . . . . . . . . . . . 12  class  j
3315cv 1622 . . . . . . . . . . . 12  class  x
3431, 32, 33co 5858 . . . . . . . . . . 11  class  ( i x j )
3529cv 1622 . . . . . . . . . . . 12  class  k
3616cv 1622 . . . . . . . . . . . 12  class  y
3732, 35, 36co 5858 . . . . . . . . . . 11  class  ( j y k )
38 cmulr 13209 . . . . . . . . . . . 12  class  .r
3917, 38cfv 5255 . . . . . . . . . . 11  class  ( .r
`  r )
4034, 37, 39co 5858 . . . . . . . . . 10  class  ( ( i x j ) ( .r `  r
) ( j y k ) )
4130, 21, 40cmpt 4077 . . . . . . . . 9  class  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) )
42 cgsu 13401 . . . . . . . . 9  class  gsumg
4317, 41, 42co 5858 . . . . . . . 8  class  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) )
4428, 29, 20, 25, 43cmpt2 5860 . . . . . . 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 5860 . . . . . 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 3081 . . . . 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 3081 . . . 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 3081 . . 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 5860 . 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 1623 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  27443
  Copyright terms: Public domain W3C validator