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 \in V, o \in V ⟼ ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvmul	$class maVecMul$
1		vr	$setvar r$
2		cvv	$class V$
3		vo	$setvar o$
4		c1st	$class 1^{st}$
5	3	cv	$setvar o$
6	5 4	cfv	$class 1^{st} (o)$
7		vm	$setvar m$
8		c2nd	$class 2^{nd}$
9	5 8	cfv	$class 2^{nd} (o)$
10		vn	$setvar n$
11		vx	$setvar x$
12		cbs	$class Base$
13	1	cv	$setvar r$
14	13 12	cfv	$class {Base}_{r}$
15		cmap	$class ↑_{𝑚}$
16	7	cv	$setvar m$
17	10	cv	$setvar n$
18	16 17	cxp	$class (m \times n)$
19	14 18 15	co	$class ({Base}_{r}^{(m \times n)})$
20		vy	$setvar y$
21	14 17 15	co	$class ({Base}_{r}^{n})$
22		vi	$setvar i$
23		cgsu	$class Σ_{𝑔}$
24		vj	$setvar j$
25	22	cv	$setvar i$
26	11	cv	$setvar x$
27	24	cv	$setvar j$
28	25 27 26	co	$class (i x j)$
29		cmulr	$class \cdot_{𝑟}$
30	13 29	cfv	$class \cdot_{r}$
31	20	cv	$setvar y$
32	27 31	cfv	$class y (j)$
33	28 32 30	co	$class ((i x j) \cdot_{r} y (j))$
34	24 17 33	cmpt	$class (j \in n ⟼ (i x j) \cdot_{r} y (j))$
35	13 34 23	co	$class (\underset{j \in n}{\sum_{r}}, ((i x j) \cdot_{r} y (j)))$
36	22 16 35	cmpt	$class (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))$
37	11 20 19 21 36	cmpo	$class (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j))))$
38	10 9 37	csb	$class ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j))))$
39	7 6 38	csb	$class ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j))))$
40	1 3 2 2 39	cmpo	$class (r \in V, o \in V ⟼ ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))))$
41	0 40	wceq	$wff maVecMul = (r \in V, o \in V ⟼ ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))))$

Metamath Proof Explorer

Definition df-mvmul

Detailed syntax breakdown