Definition df-mvmul 21598

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

Step	Hyp	Ref	Expression
1		cmvmul 21597	. 2 class maVecMul
2		vr	. . 3 setvar 𝑟
3		vo	. . 3 setvar 𝑜
4		cvv 3422	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	3	cv 1538	. . . . 5 class 𝑜
7		c1st 7802	. . . . 5 class 1st
8	6, 7	cfv 6418	. . . 4 class (1st ‘𝑜)
9		vn	. . . . 5 setvar 𝑛
10		c2nd 7803	. . . . . 6 class 2nd
11	6, 10	cfv 6418	. . . . 5 class (2nd ‘𝑜)
12		vx	. . . . . 6 setvar 𝑥
13		vy	. . . . . 6 setvar 𝑦
14	2	cv 1538	. . . . . . . 8 class 𝑟
15		cbs 16840	. . . . . . . 8 class Base
16	14, 15	cfv 6418	. . . . . . 7 class (Base‘𝑟)
17	5	cv 1538	. . . . . . . 8 class 𝑚
18	9	cv 1538	. . . . . . . 8 class 𝑛
19	17, 18	cxp 5578	. . . . . . 7 class (𝑚 × 𝑛)
20		cmap 8573	. . . . . . 7 class ↑m
21	16, 19, 20	co 7255	. . . . . 6 class ((Base‘𝑟) ↑m (𝑚 × 𝑛))
22	16, 18, 20	co 7255	. . . . . 6 class ((Base‘𝑟) ↑m 𝑛)
23		vi	. . . . . . 7 setvar 𝑖
24		vj	. . . . . . . . 9 setvar 𝑗
25	23	cv 1538	. . . . . . . . . . 11 class 𝑖
26	24	cv 1538	. . . . . . . . . . 11 class 𝑗
27	12	cv 1538	. . . . . . . . . . 11 class 𝑥
28	25, 26, 27	co 7255	. . . . . . . . . 10 class (𝑖𝑥𝑗)
29	13	cv 1538	. . . . . . . . . . 11 class 𝑦
30	26, 29	cfv 6418	. . . . . . . . . 10 class (𝑦‘𝑗)
31		cmulr 16889	. . . . . . . . . . 11 class .r
32	14, 31	cfv 6418	. . . . . . . . . 10 class (.r‘𝑟)
33	28, 30, 32	co 7255	. . . . . . . . 9 class ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))
34	24, 18, 33	cmpt 5153	. . . . . . . 8 class (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))
35		cgsu 17068	. . . . . . . 8 class Σg
36	14, 34, 35	co 7255	. . . . . . 7 class (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))
37	23, 17, 36	cmpt 5153	. . . . . 6 class (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))
38	12, 13, 21, 22, 37	cmpo 7257	. . . . 5 class (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))
39	9, 11, 38	csb 3828	. . . 4 class ⦋(2nd ‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))
40	5, 8, 39	csb 3828	. . 3 class ⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd ‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))
41	2, 3, 4, 4, 40	cmpo 7257	. 2 class (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd ‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))))
42	1, 41	wceq 1539	1 wff maVecMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd ‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))))

This definition is referenced by:  mvmulfval  21599