Definition df-mamu 22395

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.)

Assertion

Ref	Expression
df-mamu	⊢ maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd ‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))))

Distinct variable group:   𝑖,𝑗,𝑘,𝑚,𝑛,𝑜,𝑝,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-mamu

Step	Hyp	Ref	Expression
1		cmmul 22394	. 2 class maMul
2		vr	. . 3 setvar 𝑟
3		vo	. . 3 setvar 𝑜
4		cvv 3480	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	3	cv 1539	. . . . . 6 class 𝑜
7		c1st 8012	. . . . . 6 class 1st
8	6, 7	cfv 6561	. . . . 5 class (1st ‘𝑜)
9	8, 7	cfv 6561	. . . 4 class (1st ‘(1st ‘𝑜))
10		vn	. . . . 5 setvar 𝑛
11		c2nd 8013	. . . . . 6 class 2nd
12	8, 11	cfv 6561	. . . . 5 class (2nd ‘(1st ‘𝑜))
13		vp	. . . . . 6 setvar 𝑝
14	6, 11	cfv 6561	. . . . . 6 class (2nd ‘𝑜)
15		vx	. . . . . . 7 setvar 𝑥
16		vy	. . . . . . 7 setvar 𝑦
17	2	cv 1539	. . . . . . . . 9 class 𝑟
18		cbs 17247	. . . . . . . . 9 class Base
19	17, 18	cfv 6561	. . . . . . . 8 class (Base‘𝑟)
20	5	cv 1539	. . . . . . . . 9 class 𝑚
21	10	cv 1539	. . . . . . . . 9 class 𝑛
22	20, 21	cxp 5683	. . . . . . . 8 class (𝑚 × 𝑛)
23		cmap 8866	. . . . . . . 8 class ↑m
24	19, 22, 23	co 7431	. . . . . . 7 class ((Base‘𝑟) ↑m (𝑚 × 𝑛))
25	13	cv 1539	. . . . . . . . 9 class 𝑝
26	21, 25	cxp 5683	. . . . . . . 8 class (𝑛 × 𝑝)
27	19, 26, 23	co 7431	. . . . . . 7 class ((Base‘𝑟) ↑m (𝑛 × 𝑝))
28		vi	. . . . . . . 8 setvar 𝑖
29		vk	. . . . . . . 8 setvar 𝑘
30		vj	. . . . . . . . . 10 setvar 𝑗
31	28	cv 1539	. . . . . . . . . . . 12 class 𝑖
32	30	cv 1539	. . . . . . . . . . . 12 class 𝑗
33	15	cv 1539	. . . . . . . . . . . 12 class 𝑥
34	31, 32, 33	co 7431	. . . . . . . . . . 11 class (𝑖𝑥𝑗)
35	29	cv 1539	. . . . . . . . . . . 12 class 𝑘
36	16	cv 1539	. . . . . . . . . . . 12 class 𝑦
37	32, 35, 36	co 7431	. . . . . . . . . . 11 class (𝑗𝑦𝑘)
38		cmulr 17298	. . . . . . . . . . . 12 class .r
39	17, 38	cfv 6561	. . . . . . . . . . 11 class (.r‘𝑟)
40	34, 37, 39	co 7431	. . . . . . . . . 10 class ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))
41	30, 21, 40	cmpt 5225	. . . . . . . . 9 class (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))
42		cgsu 17485	. . . . . . . . 9 class Σg
43	17, 41, 42	co 7431	. . . . . . . 8 class (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))
44	28, 29, 20, 25, 43	cmpo 7433	. . . . . . 7 class (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))
45	15, 16, 24, 27, 44	cmpo 7433	. . . . . 6 class (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))
46	13, 14, 45	csb 3899	. . . . 5 class ⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))
47	10, 12, 46	csb 3899	. . . 4 class ⦋(2nd ‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))
48	5, 9, 47	csb 3899	. . 3 class ⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd ‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))
49	2, 3, 4, 4, 48	cmpo 7433	. 2 class (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd ‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))))
50	1, 49	wceq 1540	1 wff maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd ‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))))

This definition is referenced by:  mamufval  22396