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 = r ∈ V , o ∈ V ⟼ ⦋ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ o / n⦌ x ∈ Base r m × n , y ∈ Base r n ⟼ i ∈ m ⟼ ∑ r j ∈ n i x j ⋅ r y ⁡ j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvmul class maVecMul
1 vr setvar r
2 cvv class V
3 vo setvar o
4 c1st class 1 st
5 3 cv setvar o
6 5 4 cfv class 1 st ⁡ o
7 vm setvar m
8 c2nd class 2 nd
9 5 8 cfv class 2 nd ⁡ o
10 vn setvar n
11 vx setvar x
12 cbs class Base
13 1 cv setvar r
14 13 12 cfv class Base r
15 cmap class ↑ 𝑚
16 7 cv setvar m
17 10 cv setvar n
18 16 17 cxp class m × n
19 14 18 15 co class Base r m × n
20 vy setvar y
21 14 17 15 co class Base r n
22 vi setvar i
23 cgsu class Σ𝑔
24 vj setvar j
25 22 cv setvar i
26 11 cv setvar x
27 24 cv setvar j
28 25 27 26 co class i x j
29 cmulr class ⋅ 𝑟
30 13 29 cfv class ⋅ r
31 20 cv setvar y
32 27 31 cfv class y ⁡ j
33 28 32 30 co class i x j ⋅ r y ⁡ j
34 24 17 33 cmpt class j ∈ n ⟼ i x j ⋅ r y ⁡ j
35 13 34 23 co class ∑ r j ∈ n i x j ⋅ r y ⁡ j
36 22 16 35 cmpt class i ∈ m ⟼ ∑ r j ∈ n i x j ⋅ r y ⁡ j
37 11 20 19 21 36 cmpo class x ∈ Base r m × n , y ∈ Base r n ⟼ i ∈ m ⟼ ∑ r j ∈ n i x j ⋅ r y ⁡ j
38 10 9 37 csb class ⦋ 2 nd ⁡ o / n⦌ x ∈ Base r m × n , y ∈ Base r n ⟼ i ∈ m ⟼ ∑ r j ∈ n i x j ⋅ r y ⁡ j
39 7 6 38 csb class ⦋ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ o / n⦌ x ∈ Base r m × n , y ∈ Base r n ⟼ i ∈ m ⟼ ∑ r j ∈ n i x j ⋅ r y ⁡ j
40 1 3 2 2 39 cmpo class r ∈ V , o ∈ V ⟼ ⦋ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ o / n⦌ x ∈ Base r m × n , y ∈ Base r n ⟼ i ∈ m ⟼ ∑ r j ∈ n i x j ⋅ r y ⁡ j
41 0 40 wceq wff maVecMul = r ∈ V , o ∈ V ⟼ ⦋ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ o / n⦌ x ∈ Base r m × n , y ∈ Base r n ⟼ i ∈ m ⟼ ∑ r j ∈ n i x j ⋅ r y ⁡ j