Definition df-linc 42195

Description: Define the operation constructing a linear combination. Although this definition is taylored for linear combinations of vectors from left modules, it can be used for any structure having a Base, Scalar s and a scalar multiplication .s. (Contributed by AV, 29-Mar-2019.)

Assertion

Ref	Expression
df-linc	|- linC = ( m e. _V |-> ( s e. ( ( Base ` (Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsumg ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )

Distinct variable group:   m, s, v, x

Detailed syntax breakdown of Definition df-linc

Step	Hyp	Ref	Expression
1		clinc 42193	. 2 class linC
2		vm	. . 3 setvar m
3		cvv 3200	. . 3 class _V
4		vs	. . . 4 setvar s
5		vv	. . . 4 setvar v
6	2	cv 1482	. . . . . . 7 class m
7		csca 15944	. . . . . . 7 class Scalar
8	6, 7	cfv 5888	. . . . . 6 class (Scalar ` m )
9		cbs 15857	. . . . . 6 class Base
10	8, 9	cfv 5888	. . . . 5 class ( Base ` (Scalar ` m ) )
11	5	cv 1482	. . . . 5 class v
12		cmap 7857	. . . . 5 class ^m
13	10, 11, 12	co 6650	. . . 4 class ( ( Base ` (Scalar ` m ) ) ^m v )
14	6, 9	cfv 5888	. . . . 5 class ( Base ` m )
15	14	cpw 4158	. . . 4 class ~P ( Base ` m )
16		vx	. . . . . 6 setvar x
17	16	cv 1482	. . . . . . . 8 class x
18	4	cv 1482	. . . . . . . 8 class s
19	17, 18	cfv 5888	. . . . . . 7 class ( s ` x )
20		cvsca 15945	. . . . . . . 8 class .s
21	6, 20	cfv 5888	. . . . . . 7 class ( .s ` m )
22	19, 17, 21	co 6650	. . . . . 6 class ( ( s ` x ) ( .s ` m ) x )
23	16, 11, 22	cmpt 4729	. . . . 5 class ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) )
24		cgsu 16101	. . . . 5 class gsumg
25	6, 23, 24	co 6650	. . . 4 class ( m gsumg ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) )
26	4, 5, 13, 15, 25	cmpt2 6652	. . 3 class ( s e. ( ( Base ` (Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsumg ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) )
27	2, 3, 26	cmpt 4729	. 2 class ( m e. _V |-> ( s e. ( ( Base ` (Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsumg ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )
28	1, 27	wceq 1483	1 wff linC = ( m e. _V |-> ( s e. ( ( Base ` (Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsumg ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )

This definition is referenced by:  lincop  42197  dflinc2  42199