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 g
Distinct variable group:   ,,,,,,,

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