Metamath Proof Explorer

Definition df-mvmul

Description: The operator which multiplies an M x N -matrix with an N-dimensional vector. (Contributed by AV, 23-Feb-2019)

Ref Expression
Assertion 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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvmul 
 |-  maVecMul
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vo 
 |-  o
4 c1st 
 |-  1st
5 3 cv 
 |-  o
6 5 4 cfv 
 |-  ( 1st ` o )
7 vm 
 |-  m
8 c2nd 
 |-  2nd
9 5 8 cfv 
 |-  ( 2nd ` o )
10 vn 
 |-  n
11 vx 
 |-  x
12 cbs 
 |-  Base
13 1 cv 
 |-  r
14 13 12 cfv 
 |-  ( Base ` r )
15 cmap 
 |-  ^m
16 7 cv 
 |-  m
17 10 cv 
 |-  n
18 16 17 cxp 
 |-  ( m X. n )
19 14 18 15 co 
 |-  ( ( Base ` r ) ^m ( m X. n ) )
20 vy 
 |-  y
21 14 17 15 co 
 |-  ( ( Base ` r ) ^m n )
22 vi 
 |-  i
23 cgsu 
 |-  gsum
24 vj 
 |-  j
25 22 cv 
 |-  i
26 11 cv 
 |-  x
27 24 cv 
 |-  j
28 25 27 26 co 
 |-  ( i x j )
29 cmulr 
 |-  .r
30 13 29 cfv 
 |-  ( .r ` r )
31 20 cv 
 |-  y
32 27 31 cfv 
 |-  ( y ` j )
33 28 32 30 co 
 |-  ( ( i x j ) ( .r ` r ) ( y ` j ) )
34 24 17 33 cmpt 
 |-  ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) )
35 13 34 23 co 
 |-  ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) )
36 22 16 35 cmpt 
 |-  ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) )
37 11 20 19 21 36 cmpo 
 |-  ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) )
38 10 9 37 csb 
 |-  [_ ( 2nd ` o ) / n ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) )
39 7 6 38 csb 
 |-  [_ ( 1st ` o ) / m ]_ [_ ( 2nd ` o ) / n ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) )
40 1 3 2 2 39 cmpo 
 |-  ( 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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) )
41 0 40 wceq 
 |-  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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) )