Metamath Proof Explorer

Definition df-lco

Description: Define the operation constructing the set of all linear combinations for a set of vectors. (Contributed by AV, 31-Mar-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Assertion df-lco ⊢ LinCo = m ∈ V , v ∈ 𝒫 Base m ⟼ c ∈ Base m | ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v

Detailed syntax breakdown

Step Hyp Ref Expression
0 clinco class LinCo
1 vm setvar m
2 cvv class V
3 vv setvar v
4 cbs class Base
5 1 cv setvar m
6 5 4 cfv class Base m
7 6 cpw class 𝒫 Base m
8 vc setvar c
9 vs setvar s
10 csca class Scalar
11 5 10 cfv class Scalar ⁡ m
12 11 4 cfv class Base Scalar ⁡ m
13 cmap class ↑ 𝑚
14 3 cv setvar v
15 12 14 13 co class Base Scalar ⁡ m v
16 9 cv setvar s
17 cfsupp class finSupp
18 c0g class 0 𝑔
19 11 18 cfv class 0 Scalar ⁡ m
20 16 19 17 wbr wff finSupp 0 Scalar ⁡ m ⁡ s
21 8 cv setvar c
22 clinc class linC
23 5 22 cfv class linC ⁡ m
24 16 14 23 co class s linC ⁡ m v
25 21 24 wceq wff c = s linC ⁡ m v
26 20 25 wa wff finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v
27 26 9 15 wrex wff ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v
28 27 8 6 crab class c ∈ Base m | ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v
29 1 3 2 7 28 cmpo class m ∈ V , v ∈ 𝒫 Base m ⟼ c ∈ Base m | ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v
30 0 29 wceq wff LinCo = m ∈ V , v ∈ 𝒫 Base m ⟼ c ∈ Base m | ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v