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

Definition df-mvmul 20166
 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 = (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st𝑜) / 𝑚(2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))))
Distinct variable group:   𝑖,𝑗,𝑚,𝑛,𝑜,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-mvmul
StepHypRef Expression
1 cmvmul 20165 . 2 class maVecMul
2 vr . . 3 setvar 𝑟
3 vo . . 3 setvar 𝑜
4 cvv 3173 . . 3 class V
5 vm . . . 4 setvar 𝑚
63cv 1474 . . . . 5 class 𝑜
7 c1st 7057 . . . . 5 class 1st
86, 7cfv 5804 . . . 4 class (1st𝑜)
9 vn . . . . 5 setvar 𝑛
10 c2nd 7058 . . . . . 6 class 2nd
116, 10cfv 5804 . . . . 5 class (2nd𝑜)
12 vx . . . . . 6 setvar 𝑥
13 vy . . . . . 6 setvar 𝑦
142cv 1474 . . . . . . . 8 class 𝑟
15 cbs 15695 . . . . . . . 8 class Base
1614, 15cfv 5804 . . . . . . 7 class (Base‘𝑟)
175cv 1474 . . . . . . . 8 class 𝑚
189cv 1474 . . . . . . . 8 class 𝑛
1917, 18cxp 5036 . . . . . . 7 class (𝑚 × 𝑛)
20 cmap 7744 . . . . . . 7 class 𝑚
2116, 19, 20co 6549 . . . . . 6 class ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛))
2216, 18, 20co 6549 . . . . . 6 class ((Base‘𝑟) ↑𝑚 𝑛)
23 vi . . . . . . 7 setvar 𝑖
24 vj . . . . . . . . 9 setvar 𝑗
2523cv 1474 . . . . . . . . . . 11 class 𝑖
2624cv 1474 . . . . . . . . . . 11 class 𝑗
2712cv 1474 . . . . . . . . . . 11 class 𝑥
2825, 26, 27co 6549 . . . . . . . . . 10 class (𝑖𝑥𝑗)
2913cv 1474 . . . . . . . . . . 11 class 𝑦
3026, 29cfv 5804 . . . . . . . . . 10 class (𝑦𝑗)
31 cmulr 15769 . . . . . . . . . . 11 class .r
3214, 31cfv 5804 . . . . . . . . . 10 class (.r𝑟)
3328, 30, 32co 6549 . . . . . . . . 9 class ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))
3424, 18, 33cmpt 4643 . . . . . . . 8 class (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))
35 cgsu 15924 . . . . . . . 8 class Σg
3614, 34, 35co 6549 . . . . . . 7 class (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))
3723, 17, 36cmpt 4643 . . . . . 6 class (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))
3812, 13, 21, 22, 37cmpt2 6551 . . . . 5 class (𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))))
399, 11, 38csb 3499 . . . 4 class (2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))))
405, 8, 39csb 3499 . . 3 class (1st𝑜) / 𝑚(2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))))
412, 3, 4, 4, 40cmpt2 6551 . 2 class (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st𝑜) / 𝑚(2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))))
421, 41wceq 1475 1 wff maVecMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st𝑜) / 𝑚(2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))))
 Colors of variables: wff setvar class This definition is referenced by:  mvmulfval  20167
 Copyright terms: Public domain W3C validator