df-mamu

Description: The operator which multiplies an m x n matrix with an n x p matrix, see also the definition in Lang p. 504. Note that it is not generally possible to recover the dimensions from the matrix, since all n x 0 and all 0 x n matrices are represented by the empty set. (Contributed by Stefan O'Rear, 4-Sep-2015)

		Ref	Expression
	Assertion	df-mamu	$⊢ maMul = (r \in V, o \in V ⟼ ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmmul	$class maMul$
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	6 4	cfv	$class 1^{st} (1^{st} (o))$
8		vm	$setvar m$
9		c2nd	$class 2^{nd}$
10	6 9	cfv	$class 2^{nd} (1^{st} (o))$
11		vn	$setvar n$
12	5 9	cfv	$class 2^{nd} (o)$
13		vp	$setvar p$
14		vx	$setvar x$
15		cbs	$class Base$
16	1	cv	$setvar r$
17	16 15	cfv	$class {Base}_{r}$
18		cmap	$class ↑_{𝑚}$
19	8	cv	$setvar m$
20	11	cv	$setvar n$
21	19 20	cxp	$class (m \times n)$
22	17 21 18	co	$class ({Base}_{r}^{(m \times n)})$
23		vy	$setvar y$
24	13	cv	$setvar p$
25	20 24	cxp	$class (n \times p)$
26	17 25 18	co	$class ({Base}_{r}^{(n \times p)})$
27		vi	$setvar i$
28		vk	$setvar k$
29		cgsu	$class Σ_{𝑔}$
30		vj	$setvar j$
31	27	cv	$setvar i$
32	14	cv	$setvar x$
33	30	cv	$setvar j$
34	31 33 32	co	$class (i x j)$
35		cmulr	$class \cdot_{𝑟}$
36	16 35	cfv	$class \cdot_{r}$
37	23	cv	$setvar y$
38	28	cv	$setvar k$
39	33 38 37	co	$class (j y k)$
40	34 39 36	co	$class ((i x j) \cdot_{r} (j y k))$
41	30 20 40	cmpt	$class (j \in n ⟼ (i x j) \cdot_{r} (j y k))$
42	16 41 29	co	$class (\underset{j \in n}{\sum_{r}}, ((i x j) \cdot_{r} (j y k)))$
43	27 28 19 24 42	cmpo	$class (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))$
44	14 23 22 26 43	cmpo	$class (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
45	13 12 44	csb	$class ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
46	11 10 45	csb	$class ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
47	8 7 46	csb	$class ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
48	1 3 2 2 47	cmpo	$class (r \in V, o \in V ⟼ ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))))$
49	0 48	wceq	$wff maMul = (r \in V, o \in V ⟼ ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))))$

Metamath Proof Explorer

Definition df-mamu

Detailed syntax breakdown