Metamath Proof Explorer


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𝑟 ) ( 𝑦𝑗 ) ) ) ) ) ) )