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

Definition df-mamu 27456
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 27454 . 2  class maMul
2 vr . . 3  set  r
3 vo . . 3  set  o
4 cvv 2962 . . 3  class  _V
5 vm . . . 4  set  m
63cv 1652 . . . . . 6  class  o
7 c1st 6376 . . . . . 6  class  1st
86, 7cfv 5483 . . . . 5  class  ( 1st `  o )
98, 7cfv 5483 . . . 4  class  ( 1st `  ( 1st `  o
) )
10 vn . . . . 5  set  n
11 c2nd 6377 . . . . . 6  class  2nd
128, 11cfv 5483 . . . . 5  class  ( 2nd `  ( 1st `  o
) )
13 vp . . . . . 6  set  p
146, 11cfv 5483 . . . . . 6  class  ( 2nd `  o )
15 vx . . . . . . 7  set  x
16 vy . . . . . . 7  set  y
172cv 1652 . . . . . . . . 9  class  r
18 cbs 13500 . . . . . . . . 9  class  Base
1917, 18cfv 5483 . . . . . . . 8  class  ( Base `  r )
205cv 1652 . . . . . . . . 9  class  m
2110cv 1652 . . . . . . . . 9  class  n
2220, 21cxp 4905 . . . . . . . 8  class  ( m  X.  n )
23 cmap 7047 . . . . . . . 8  class  ^m
2419, 22, 23co 6110 . . . . . . 7  class  ( (
Base `  r )  ^m  ( m  X.  n
) )
2513cv 1652 . . . . . . . . 9  class  p
2621, 25cxp 4905 . . . . . . . 8  class  ( n  X.  p )
2719, 26, 23co 6110 . . . . . . 7  class  ( (
Base `  r )  ^m  ( n  X.  p
) )
28 vi . . . . . . . 8  set  i
29 vk . . . . . . . 8  set  k
30 vj . . . . . . . . . 10  set  j
3128cv 1652 . . . . . . . . . . . 12  class  i
3230cv 1652 . . . . . . . . . . . 12  class  j
3315cv 1652 . . . . . . . . . . . 12  class  x
3431, 32, 33co 6110 . . . . . . . . . . 11  class  ( i x j )
3529cv 1652 . . . . . . . . . . . 12  class  k
3616cv 1652 . . . . . . . . . . . 12  class  y
3732, 35, 36co 6110 . . . . . . . . . . 11  class  ( j y k )
38 cmulr 13561 . . . . . . . . . . . 12  class  .r
3917, 38cfv 5483 . . . . . . . . . . 11  class  ( .r
`  r )
4034, 37, 39co 6110 . . . . . . . . . 10  class  ( ( i x j ) ( .r `  r
) ( j y k ) )
4130, 21, 40cmpt 4291 . . . . . . . . 9  class  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) )
42 cgsu 13755 . . . . . . . . 9  class  gsumg
4317, 41, 42co 6110 . . . . . . . 8  class  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) )
4428, 29, 20, 25, 43cmpt2 6112 . . . . . . 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 6112 . . . . . 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 3267 . . . . 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 3267 . . . 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 3267 . . 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 6112 . 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 1653 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  27458
  Copyright terms: Public domain W3C validator