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 ·_𝑠. (Contributed by AV, 29-Mar-2019.)

Assertion

Ref	Expression
df-linc	⊢ linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))

Distinct variable group:   𝑚,𝑠,𝑣,𝑥

Detailed syntax breakdown of Definition df-linc

Step	Hyp	Ref	Expression
1		clinc 42193	. 2 class linC
2		vm	. . 3 setvar 𝑚
3		cvv 3200	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5		vv	. . . 4 setvar 𝑣
6	2	cv 1482	. . . . . . 7 class 𝑚
7		csca 15944	. . . . . . 7 class Scalar
8	6, 7	cfv 5888	. . . . . 6 class (Scalar‘𝑚)
9		cbs 15857	. . . . . 6 class Base
10	8, 9	cfv 5888	. . . . 5 class (Base‘(Scalar‘𝑚))
11	5	cv 1482	. . . . 5 class 𝑣
12		cmap 7857	. . . . 5 class ↑𝑚
13	10, 11, 12	co 6650	. . . 4 class ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)
14	6, 9	cfv 5888	. . . . 5 class (Base‘𝑚)
15	14	cpw 4158	. . . 4 class 𝒫 (Base‘𝑚)
16		vx	. . . . . 6 setvar 𝑥
17	16	cv 1482	. . . . . . . 8 class 𝑥
18	4	cv 1482	. . . . . . . 8 class 𝑠
19	17, 18	cfv 5888	. . . . . . 7 class (𝑠‘𝑥)
20		cvsca 15945	. . . . . . . 8 class ·𝑠
21	6, 20	cfv 5888	. . . . . . 7 class ( ·𝑠 ‘𝑚)
22	19, 17, 21	co 6650	. . . . . 6 class ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)
23	16, 11, 22	cmpt 4729	. . . . 5 class (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))
24		cgsu 16101	. . . . 5 class Σg
25	6, 23, 24	co 6650	. . . 4 class (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))
26	4, 5, 13, 15, 25	cmpt2 6652	. . 3 class (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))))
27	2, 3, 26	cmpt 4729	. 2 class (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))
28	1, 27	wceq 1483	1 wff linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))

This definition is referenced by:  lincop  42197  dflinc2  42199