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

Detailed syntax breakdown

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