Definition 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 = ( 𝑟 ∈ V , 𝑜 ∈ V ↦ ⦋ ( 1st ‘ ( 1st ‘ 𝑜 ) ) / 𝑚 ⦌ ⦋ ( 2nd ‘ ( 1st ‘ 𝑜 ) ) / 𝑛 ⦌ ⦋ ( 2nd ‘ 𝑜 ) / 𝑝 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )

Detailed syntax breakdown

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