Metamath Proof Explorer

Definition df-linc

Description: Define the operation constructing a linear combination. Although this definition is taylored for linear combinations of vectors from left modules, it can be used for any structure having a Base , Scalar s and a scalar multiplication .s . (Contributed by AV, 29-Mar-2019)

Ref Expression
Assertion df-linc ⊢ linC = m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m x ∈ v s ⁡ x ⋅ m x

Detailed syntax breakdown

Step Hyp Ref Expression
0 clinc class linC
1 vm setvar m
2 cvv class V
3 vs setvar s
4 cbs class Base
5 csca class Scalar
6 1 cv setvar m
7 6 5 cfv class Scalar ⁡ m
8 7 4 cfv class Base Scalar ⁡ m
9 cmap class ↑ 𝑚
10 vv setvar v
11 10 cv setvar v
12 8 11 9 co class Base Scalar ⁡ m v
13 6 4 cfv class Base m
14 13 cpw class 𝒫 Base m
15 cgsu class Σ𝑔
16 vx setvar x
17 3 cv setvar s
18 16 cv setvar x
19 18 17 cfv class s ⁡ x
20 cvsca class ⋅ 𝑠
21 6 20 cfv class ⋅ m
22 19 18 21 co class s ⁡ x ⋅ m x
23 16 11 22 cmpt class x ∈ v ⟼ s ⁡ x ⋅ m x
24 6 23 15 co class ∑ m x ∈ v s ⁡ x ⋅ m x
25 3 10 12 14 24 cmpo class s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m x ∈ v s ⁡ x ⋅ m x
26 1 2 25 cmpt class m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m x ∈ v s ⁡ x ⋅ m x
27 0 26 wceq wff linC = m ∈ V ⟼ s ∈ Base Scalar ⁡ m v , v ∈ 𝒫 Base m ⟼ ∑ m x ∈ v s ⁡ x ⋅ m x