Definition df-lco 42196

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 = ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` (Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` (Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )

Distinct variable group:   m, c, s, v

Detailed syntax breakdown of Definition df-lco

Step	Hyp	Ref	Expression
1		clinco 42194	. 2 class LinCo
2		vm	. . 3 setvar m
3		vv	. . 3 setvar v
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class m
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` m )
8	7	cpw 4158	. . 3 class ~P ( Base ` m )
9		vs	. . . . . . . 8 setvar s
10	9	cv 1482	. . . . . . 7 class s
11		csca 15944	. . . . . . . . 9 class Scalar
12	5, 11	cfv 5888	. . . . . . . 8 class (Scalar ` m )
13		c0g 16100	. . . . . . . 8 class 0g
14	12, 13	cfv 5888	. . . . . . 7 class ( 0g ` (Scalar ` m ) )
15		cfsupp 8275	. . . . . . 7 class finSupp
16	10, 14, 15	wbr 4653	. . . . . 6 wff s finSupp ( 0g ` (Scalar ` m ) )
17		vc	. . . . . . . 8 setvar c
18	17	cv 1482	. . . . . . 7 class c
19	3	cv 1482	. . . . . . . 8 class v
20		clinc 42193	. . . . . . . . 9 class linC
21	5, 20	cfv 5888	. . . . . . . 8 class ( linC ` m )
22	10, 19, 21	co 6650	. . . . . . 7 class ( s ( linC ` m ) v )
23	18, 22	wceq 1483	. . . . . 6 wff c = ( s ( linC ` m ) v )
24	16, 23	wa 384	. . . . 5 wff ( s finSupp ( 0g ` (Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) )
25	12, 6	cfv 5888	. . . . . 6 class ( Base ` (Scalar ` m ) )
26		cmap 7857	. . . . . 6 class ^m
27	25, 19, 26	co 6650	. . . . 5 class ( ( Base ` (Scalar ` m ) ) ^m v )
28	24, 9, 27	wrex 2913	. . . 4 wff E. s e. ( ( Base ` (Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` (Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) )
29	28, 17, 7	crab 2916	. . 3 class { c e. ( Base ` m ) | E. s e. ( ( Base ` (Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` (Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) }
30	2, 3, 4, 8, 29	cmpt2 6652	. 2 class ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` (Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` (Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )
31	1, 30	wceq 1483	1 wff LinCo = ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` (Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` (Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )

This definition is referenced by:  lcoop  42200