Definition df-lco 44482

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 44480	. 2 class LinCo
2		vm	. . 3 setvar 𝑚
3		vv	. . 3 setvar 𝑣
4		cvv 3494	. . 3 class V
5	2	cv 1536	. . . . 5 class 𝑚
6		cbs 16483	. . . . 5 class Base
7	5, 6	cfv 6355	. . . 4 class (Base‘𝑚)
8	7	cpw 4539	. . 3 class 𝒫 (Base‘𝑚)
9		vs	. . . . . . . 8 setvar 𝑠
10	9	cv 1536	. . . . . . 7 class 𝑠
11		csca 16568	. . . . . . . . 9 class Scalar
12	5, 11	cfv 6355	. . . . . . . 8 class (Scalar‘𝑚)
13		c0g 16713	. . . . . . . 8 class 0g
14	12, 13	cfv 6355	. . . . . . 7 class (0g‘(Scalar‘𝑚))
15		cfsupp 8833	. . . . . . 7 class finSupp
16	10, 14, 15	wbr 5066	. . . . . 6 wff 𝑠 finSupp (0g‘(Scalar‘𝑚))
17		vc	. . . . . . . 8 setvar 𝑐
18	17	cv 1536	. . . . . . 7 class 𝑐
19	3	cv 1536	. . . . . . . 8 class 𝑣
20		clinc 44479	. . . . . . . . 9 class linC
21	5, 20	cfv 6355	. . . . . . . 8 class ( linC ‘𝑚)
22	10, 19, 21	co 7156	. . . . . . 7 class (𝑠( linC ‘𝑚)𝑣)
23	18, 22	wceq 1537	. . . . . 6 wff 𝑐 = (𝑠( linC ‘𝑚)𝑣)
24	16, 23	wa 398	. . . . 5 wff (𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
25	12, 6	cfv 6355	. . . . . 6 class (Base‘(Scalar‘𝑚))
26		cmap 8406	. . . . . 6 class ↑m
27	25, 19, 26	co 7156	. . . . 5 class ((Base‘(Scalar‘𝑚)) ↑m 𝑣)
28	24, 9, 27	wrex 3139	. . . 4 wff ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))
29	28, 17, 7	crab 3142	. . 3 class {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}
30	2, 3, 4, 8, 29	cmpo 7158	. 2 class (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
31	1, 30	wceq 1537	1 wff LinCo = (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})

This definition is referenced by:  lcoop  44486