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

Definition df-mvmul 18465
Description: The operator which multiplies an M x N -matrix with an N-dimensional vector. (Contributed by AV, 23-Feb-2019.)
Assertion
Ref Expression
df-mvmul  |- maVecMul  =  ( r  e.  _V , 
o  e.  _V  |->  [_ ( 1st `  o )  /  m ]_ [_ ( 2nd `  o )  /  n ]_ ( x  e.  ( ( Base `  r
)  ^m  ( m  X.  n ) ) ,  y  e.  ( (
Base `  r )  ^m  n )  |->  ( i  e.  m  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) ) ) ) )
Distinct variable group:    i, j, m, n, o, r, x, y

Detailed syntax breakdown of Definition df-mvmul
StepHypRef Expression
1 cmvmul 18464 . 2  class maVecMul
2 vr . . 3  setvar  r
3 vo . . 3  setvar  o
4 cvv 3070 . . 3  class  _V
5 vm . . . 4  setvar  m
63cv 1369 . . . . 5  class  o
7 c1st 6677 . . . . 5  class  1st
86, 7cfv 5518 . . . 4  class  ( 1st `  o )
9 vn . . . . 5  setvar  n
10 c2nd 6678 . . . . . 6  class  2nd
116, 10cfv 5518 . . . . 5  class  ( 2nd `  o )
12 vx . . . . . 6  setvar  x
13 vy . . . . . 6  setvar  y
142cv 1369 . . . . . . . 8  class  r
15 cbs 14278 . . . . . . . 8  class  Base
1614, 15cfv 5518 . . . . . . 7  class  ( Base `  r )
175cv 1369 . . . . . . . 8  class  m
189cv 1369 . . . . . . . 8  class  n
1917, 18cxp 4938 . . . . . . 7  class  ( m  X.  n )
20 cmap 7316 . . . . . . 7  class  ^m
2116, 19, 20co 6192 . . . . . 6  class  ( (
Base `  r )  ^m  ( m  X.  n
) )
2216, 18, 20co 6192 . . . . . 6  class  ( (
Base `  r )  ^m  n )
23 vi . . . . . . 7  setvar  i
24 vj . . . . . . . . 9  setvar  j
2523cv 1369 . . . . . . . . . . 11  class  i
2624cv 1369 . . . . . . . . . . 11  class  j
2712cv 1369 . . . . . . . . . . 11  class  x
2825, 26, 27co 6192 . . . . . . . . . 10  class  ( i x j )
2913cv 1369 . . . . . . . . . . 11  class  y
3026, 29cfv 5518 . . . . . . . . . 10  class  ( y `
 j )
31 cmulr 14343 . . . . . . . . . . 11  class  .r
3214, 31cfv 5518 . . . . . . . . . 10  class  ( .r
`  r )
3328, 30, 32co 6192 . . . . . . . . 9  class  ( ( i x j ) ( .r `  r
) ( y `  j ) )
3424, 18, 33cmpt 4450 . . . . . . . 8  class  ( j  e.  n  |->  ( ( i x j ) ( .r `  r
) ( y `  j ) ) )
35 cgsu 14483 . . . . . . . 8  class  gsumg
3614, 34, 35co 6192 . . . . . . 7  class  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) )
3723, 17, 36cmpt 4450 . . . . . 6  class  ( i  e.  m  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) ) )
3812, 13, 21, 22, 37cmpt2 6194 . . . . 5  class  ( x  e.  ( ( Base `  r )  ^m  (
m  X.  n ) ) ,  y  e.  ( ( Base `  r
)  ^m  n )  |->  ( i  e.  m  |->  ( r  gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) ) ) )
399, 11, 38csb 3388 . . . 4  class  [_ ( 2nd `  o )  /  n ]_ ( x  e.  ( ( Base `  r
)  ^m  ( m  X.  n ) ) ,  y  e.  ( (
Base `  r )  ^m  n )  |->  ( i  e.  m  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) ) ) )
405, 8, 39csb 3388 . . 3  class  [_ ( 1st `  o )  /  m ]_ [_ ( 2nd `  o )  /  n ]_ ( x  e.  ( ( Base `  r
)  ^m  ( m  X.  n ) ) ,  y  e.  ( (
Base `  r )  ^m  n )  |->  ( i  e.  m  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) ) ) )
412, 3, 4, 4, 40cmpt2 6194 . 2  class  ( r  e.  _V ,  o  e.  _V  |->  [_ ( 1st `  o )  /  m ]_ [_ ( 2nd `  o )  /  n ]_ ( x  e.  ( ( Base `  r
)  ^m  ( m  X.  n ) ) ,  y  e.  ( (
Base `  r )  ^m  n )  |->  ( i  e.  m  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) ) ) ) )
421, 41wceq 1370 1  wff maVecMul  =  ( r  e.  _V , 
o  e.  _V  |->  [_ ( 1st `  o )  /  m ]_ [_ ( 2nd `  o )  /  n ]_ ( x  e.  ( ( Base `  r
)  ^m  ( m  X.  n ) ) ,  y  e.  ( (
Base `  r )  ^m  n )  |->  ( i  e.  m  |->  ( r 
gsumg  ( j  e.  n  |->  ( ( i x j ) ( .r
`  r ) ( y `  j ) ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mvmulfval  18466
  Copyright terms: Public domain W3C validator