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

Definition df-mvmul 21149
 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‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))))
Distinct variable group:   𝑖,𝑗,𝑚,𝑛,𝑜,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-mvmul
StepHypRef Expression
1 cmvmul 21148 . 2 class maVecMul
2 vr . . 3 setvar 𝑟
3 vo . . 3 setvar 𝑜
4 cvv 3444 . . 3 class V
5 vm . . . 4 setvar 𝑚
63cv 1537 . . . . 5 class 𝑜
7 c1st 7673 . . . . 5 class 1st
86, 7cfv 6328 . . . 4 class (1st𝑜)
9 vn . . . . 5 setvar 𝑛
10 c2nd 7674 . . . . . 6 class 2nd
116, 10cfv 6328 . . . . 5 class (2nd𝑜)
12 vx . . . . . 6 setvar 𝑥
13 vy . . . . . 6 setvar 𝑦
142cv 1537 . . . . . . . 8 class 𝑟
15 cbs 16478 . . . . . . . 8 class Base
1614, 15cfv 6328 . . . . . . 7 class (Base‘𝑟)
175cv 1537 . . . . . . . 8 class 𝑚
189cv 1537 . . . . . . . 8 class 𝑛
1917, 18cxp 5521 . . . . . . 7 class (𝑚 × 𝑛)
20 cmap 8393 . . . . . . 7 class m
2116, 19, 20co 7139 . . . . . 6 class ((Base‘𝑟) ↑m (𝑚 × 𝑛))
2216, 18, 20co 7139 . . . . . 6 class ((Base‘𝑟) ↑m 𝑛)
23 vi . . . . . . 7 setvar 𝑖
24 vj . . . . . . . . 9 setvar 𝑗
2523cv 1537 . . . . . . . . . . 11 class 𝑖
2624cv 1537 . . . . . . . . . . 11 class 𝑗
2712cv 1537 . . . . . . . . . . 11 class 𝑥
2825, 26, 27co 7139 . . . . . . . . . 10 class (𝑖𝑥𝑗)
2913cv 1537 . . . . . . . . . . 11 class 𝑦
3026, 29cfv 6328 . . . . . . . . . 10 class (𝑦𝑗)
31 cmulr 16561 . . . . . . . . . . 11 class .r
3214, 31cfv 6328 . . . . . . . . . 10 class (.r𝑟)
3328, 30, 32co 7139 . . . . . . . . 9 class ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))
3424, 18, 33cmpt 5113 . . . . . . . 8 class (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))
35 cgsu 16709 . . . . . . . 8 class Σg
3614, 34, 35co 7139 . . . . . . 7 class (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))
3723, 17, 36cmpt 5113 . . . . . 6 class (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))
3812, 13, 21, 22, 37cmpo 7141 . . . . 5 class (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))))
399, 11, 38csb 3831 . . . 4 class (2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))))
405, 8, 39csb 3831 . . 3 class (1st𝑜) / 𝑚(2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗))))))
412, 3, 4, 4, 40cmpo 7141 . 2 class (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st𝑜) / 𝑚(2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))))
421, 41wceq 1538 1 wff maVecMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st𝑜) / 𝑚(2nd𝑜) / 𝑛(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖𝑚 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑦𝑗)))))))
 Colors of variables: wff setvar class This definition is referenced by:  mvmulfval  21150
 Copyright terms: Public domain W3C validator