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 \in V, v \in 𝒫 {Base}_{m} ⟼ \{c \in {Base}_{m} \| \exists s \in ({Base}_{Scalar (m)}^{v}) ({finSupp}_{0_{Scalar (m)}} (s) \land 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) \land c = s linC (m) v)$
27	26 9 15	wrex	$wff \exists s \in ({Base}_{Scalar (m)}^{v}) ({finSupp}_{0_{Scalar (m)}} (s) \land c = s linC (m) v)$
28	27 8 6	crab	$class \{c \in {Base}_{m} \| \exists s \in ({Base}_{Scalar (m)}^{v}) ({finSupp}_{0_{Scalar (m)}} (s) \land c = s linC (m) v)\}$
29	1 3 2 7 28	cmpo	$class (m \in V, v \in 𝒫 {Base}_{m} ⟼ \{c \in {Base}_{m} \| \exists s \in ({Base}_{Scalar (m)}^{v}) ({finSupp}_{0_{Scalar (m)}} (s) \land c = s linC (m) v)\})$
30	0 29	wceq	$wff LinCo = (m \in V, v \in 𝒫 {Base}_{m} ⟼ \{c \in {Base}_{m} \| \exists s \in ({Base}_{Scalar (m)}^{v}) ({finSupp}_{0_{Scalar (m)}} (s) \land c = s linC (m) v)\})$

Metamath Proof Explorer

Definition df-lco

Detailed syntax breakdown