Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lco Structured version   Visualization version   GIF version

Definition df-lco 44811
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.)
Assertion
Ref Expression
df-lco LinCo = (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
Distinct variable group:   𝑚,𝑐,𝑠,𝑣

Detailed syntax breakdown of Definition df-lco
StepHypRef Expression
1 clinco 44809 . 2 class LinCo
2 vm . . 3 setvar 𝑚
3 vv . . 3 setvar 𝑣
4 cvv 3441 . . 3 class V
52cv 1537 . . . . 5 class 𝑚
6 cbs 16475 . . . . 5 class Base
75, 6cfv 6324 . . . 4 class (Base‘𝑚)
87cpw 4497 . . 3 class 𝒫 (Base‘𝑚)
9 vs . . . . . . . 8 setvar 𝑠
109cv 1537 . . . . . . 7 class 𝑠
11 csca 16560 . . . . . . . . 9 class Scalar
125, 11cfv 6324 . . . . . . . 8 class (Scalar‘𝑚)
13 c0g 16705 . . . . . . . 8 class 0g
1412, 13cfv 6324 . . . . . . 7 class (0g‘(Scalar‘𝑚))
15 cfsupp 8817 . . . . . . 7 class finSupp
1610, 14, 15wbr 5030 . . . . . 6 wff 𝑠 finSupp (0g‘(Scalar‘𝑚))
17 vc . . . . . . . 8 setvar 𝑐
1817cv 1537 . . . . . . 7 class 𝑐
193cv 1537 . . . . . . . 8 class 𝑣
20 clinc 44808 . . . . . . . . 9 class linC
215, 20cfv 6324 . . . . . . . 8 class ( linC ‘𝑚)
2210, 19, 21co 7135 . . . . . . 7 class (𝑠( linC ‘𝑚)𝑣)
2318, 22wceq 1538 . . . . . 6 wff 𝑐 = (𝑠( linC ‘𝑚)𝑣)
2416, 23wa 399 . . . . 5 wff (𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
2512, 6cfv 6324 . . . . . 6 class (Base‘(Scalar‘𝑚))
26 cmap 8389 . . . . . 6 class m
2725, 19, 26co 7135 . . . . 5 class ((Base‘(Scalar‘𝑚)) ↑m 𝑣)
2824, 9, 27wrex 3107 . . . 4 wff 𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
2928, 17, 7crab 3110 . . 3 class {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}
302, 3, 4, 8, 29cmpo 7137 . 2 class (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
311, 30wceq 1538 1 wff LinCo = (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
Colors of variables: wff setvar class
This definition is referenced by:  lcoop  44815
  Copyright terms: Public domain W3C validator