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 41967
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‘𝑚)) ↑𝑚 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
Distinct variable group:   𝑚,𝑐,𝑠,𝑣

Detailed syntax breakdown of Definition df-lco
StepHypRef Expression
1 clinco 41965 . 2 class LinCo
2 vm . . 3 setvar 𝑚
3 vv . . 3 setvar 𝑣
4 cvv 3198 . . 3 class V
52cv 1481 . . . . 5 class 𝑚
6 cbs 15851 . . . . 5 class Base
75, 6cfv 5886 . . . 4 class (Base‘𝑚)
87cpw 4156 . . 3 class 𝒫 (Base‘𝑚)
9 vs . . . . . . . 8 setvar 𝑠
109cv 1481 . . . . . . 7 class 𝑠
11 csca 15938 . . . . . . . . 9 class Scalar
125, 11cfv 5886 . . . . . . . 8 class (Scalar‘𝑚)
13 c0g 16094 . . . . . . . 8 class 0g
1412, 13cfv 5886 . . . . . . 7 class (0g‘(Scalar‘𝑚))
15 cfsupp 8272 . . . . . . 7 class finSupp
1610, 14, 15wbr 4651 . . . . . 6 wff 𝑠 finSupp (0g‘(Scalar‘𝑚))
17 vc . . . . . . . 8 setvar 𝑐
1817cv 1481 . . . . . . 7 class 𝑐
193cv 1481 . . . . . . . 8 class 𝑣
20 clinc 41964 . . . . . . . . 9 class linC
215, 20cfv 5886 . . . . . . . 8 class ( linC ‘𝑚)
2210, 19, 21co 6647 . . . . . . 7 class (𝑠( linC ‘𝑚)𝑣)
2318, 22wceq 1482 . . . . . 6 wff 𝑐 = (𝑠( linC ‘𝑚)𝑣)
2416, 23wa 384 . . . . 5 wff (𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
2512, 6cfv 5886 . . . . . 6 class (Base‘(Scalar‘𝑚))
26 cmap 7854 . . . . . 6 class 𝑚
2725, 19, 26co 6647 . . . . 5 class ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)
2824, 9, 27wrex 2912 . . . 4 wff 𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
2928, 17, 7crab 2915 . . 3 class {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}
302, 3, 4, 8, 29cmpt2 6649 . 2 class (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
311, 30wceq 1482 1 wff LinCo = (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
Colors of variables: wff setvar class
This definition is referenced by:  lcoop  41971
  Copyright terms: Public domain W3C validator