MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mamu Structured version   Unicode version

Definition df-mamu 18280
Description: The operator which multiplies an m x n matrix with an n x p matrix, see also the definition in [Lang] p. 504. Note that it is not generally possible to recover the dimensions from the matrix, since all n x 0 and all 0 x n 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 18278 . 2  class maMul
2 vr . . 3  setvar  r
3 vo . . 3  setvar  o
4 cvv 2971 . . 3  class  _V
5 vm . . . 4  setvar  m
63cv 1368 . . . . . 6  class  o
7 c1st 6574 . . . . . 6  class  1st
86, 7cfv 5417 . . . . 5  class  ( 1st `  o )
98, 7cfv 5417 . . . 4  class  ( 1st `  ( 1st `  o
) )
10 vn . . . . 5  setvar  n
11 c2nd 6575 . . . . . 6  class  2nd
128, 11cfv 5417 . . . . 5  class  ( 2nd `  ( 1st `  o
) )
13 vp . . . . . 6  setvar  p
146, 11cfv 5417 . . . . . 6  class  ( 2nd `  o )
15 vx . . . . . . 7  setvar  x
16 vy . . . . . . 7  setvar  y
172cv 1368 . . . . . . . . 9  class  r
18 cbs 14173 . . . . . . . . 9  class  Base
1917, 18cfv 5417 . . . . . . . 8  class  ( Base `  r )
205cv 1368 . . . . . . . . 9  class  m
2110cv 1368 . . . . . . . . 9  class  n
2220, 21cxp 4837 . . . . . . . 8  class  ( m  X.  n )
23 cmap 7213 . . . . . . . 8  class  ^m
2419, 22, 23co 6090 . . . . . . 7  class  ( (
Base `  r )  ^m  ( m  X.  n
) )
2513cv 1368 . . . . . . . . 9  class  p
2621, 25cxp 4837 . . . . . . . 8  class  ( n  X.  p )
2719, 26, 23co 6090 . . . . . . 7  class  ( (
Base `  r )  ^m  ( n  X.  p
) )
28 vi . . . . . . . 8  setvar  i
29 vk . . . . . . . 8  setvar  k
30 vj . . . . . . . . . 10  setvar  j
3128cv 1368 . . . . . . . . . . . 12  class  i
3230cv 1368 . . . . . . . . . . . 12  class  j
3315cv 1368 . . . . . . . . . . . 12  class  x
3431, 32, 33co 6090 . . . . . . . . . . 11  class  ( i x j )
3529cv 1368 . . . . . . . . . . . 12  class  k
3616cv 1368 . . . . . . . . . . . 12  class  y
3732, 35, 36co 6090 . . . . . . . . . . 11  class  ( j y k )
38 cmulr 14238 . . . . . . . . . . . 12  class  .r
3917, 38cfv 5417 . . . . . . . . . . 11  class  ( .r
`  r )
4034, 37, 39co 6090 . . . . . . . . . 10  class  ( ( i x j ) ( .r `  r
) ( j y k ) )
4130, 21, 40cmpt 4349 . . . . . . . . 9  class  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( j y k ) ) )
42 cgsu 14378 . . . . . . . . 9  class  gsumg
4317, 41, 42co 6090 . . . . . . . 8  class  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( j y k ) ) ) )
4428, 29, 20, 25, 43cmpt2 6092 . . . . . . 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 6092 . . . . . 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 3287 . . . . 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 3287 . . . 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 3287 . . 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 6092 . 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 1369 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 setvar class
This definition is referenced by:  mamufval  18282
  Copyright terms: Public domain W3C validator