This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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