Definition df-lco 45700

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

Step	Hyp	Ref	Expression
1		clinco 45698	. 2 class LinCo
2		vm	. . 3 setvar 𝑚
3		vv	. . 3 setvar 𝑣
4		cvv 3430	. . 3 class V
5	2	cv 1540	. . . . 5 class 𝑚
6		cbs 16893	. . . . 5 class Base
7	5, 6	cfv 6430	. . . 4 class (Base‘𝑚)
8	7	cpw 4538	. . 3 class 𝒫 (Base‘𝑚)
9		vs	. . . . . . . 8 setvar 𝑠
10	9	cv 1540	. . . . . . 7 class 𝑠
11		csca 16946	. . . . . . . . 9 class Scalar
12	5, 11	cfv 6430	. . . . . . . 8 class (Scalar‘𝑚)
13		c0g 17131	. . . . . . . 8 class 0g
14	12, 13	cfv 6430	. . . . . . 7 class (0g‘(Scalar‘𝑚))
15		cfsupp 9089	. . . . . . 7 class finSupp
16	10, 14, 15	wbr 5078	. . . . . 6 wff 𝑠 finSupp (0g‘(Scalar‘𝑚))
17		vc	. . . . . . . 8 setvar 𝑐
18	17	cv 1540	. . . . . . 7 class 𝑐
19	3	cv 1540	. . . . . . . 8 class 𝑣
20		clinc 45697	. . . . . . . . 9 class linC
21	5, 20	cfv 6430	. . . . . . . 8 class ( linC ‘𝑚)
22	10, 19, 21	co 7268	. . . . . . 7 class (𝑠( linC ‘𝑚)𝑣)
23	18, 22	wceq 1541	. . . . . 6 wff 𝑐 = (𝑠( linC ‘𝑚)𝑣)
24	16, 23	wa 395	. . . . 5 wff (𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
25	12, 6	cfv 6430	. . . . . 6 class (Base‘(Scalar‘𝑚))
26		cmap 8589	. . . . . 6 class ↑m
27	25, 19, 26	co 7268	. . . . 5 class ((Base‘(Scalar‘𝑚)) ↑m 𝑣)
28	24, 9, 27	wrex 3066	. . . 4 wff ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
29	28, 17, 7	crab 3069	. . 3 class {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}
30	2, 3, 4, 8, 29	cmpo 7270	. 2 class (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
31	1, 30	wceq 1541	1 wff LinCo = (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})

This definition is referenced by:  lcoop  45704