Definition df-linc 47041

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‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))

Distinct variable group:   𝑚,𝑠,𝑣,𝑥

Detailed syntax breakdown of Definition df-linc

Step	Hyp	Ref	Expression
1		clinc 47039	. 2 class linC
2		vm	. . 3 setvar 𝑚
3		cvv 3475	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5		vv	. . . 4 setvar 𝑣
6	2	cv 1541	. . . . . . 7 class 𝑚
7		csca 17197	. . . . . . 7 class Scalar
8	6, 7	cfv 6541	. . . . . 6 class (Scalar‘𝑚)
9		cbs 17141	. . . . . 6 class Base
10	8, 9	cfv 6541	. . . . 5 class (Base‘(Scalar‘𝑚))
11	5	cv 1541	. . . . 5 class 𝑣
12		cmap 8817	. . . . 5 class ↑m
13	10, 11, 12	co 7406	. . . 4 class ((Base‘(Scalar‘𝑚)) ↑m 𝑣)
14	6, 9	cfv 6541	. . . . 5 class (Base‘𝑚)
15	14	cpw 4602	. . . 4 class 𝒫 (Base‘𝑚)
16		vx	. . . . . 6 setvar 𝑥
17	16	cv 1541	. . . . . . . 8 class 𝑥
18	4	cv 1541	. . . . . . . 8 class 𝑠
19	17, 18	cfv 6541	. . . . . . 7 class (𝑠‘𝑥)
20		cvsca 17198	. . . . . . . 8 class ·𝑠
21	6, 20	cfv 6541	. . . . . . 7 class ( ·𝑠 ‘𝑚)
22	19, 17, 21	co 7406	. . . . . 6 class ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)
23	16, 11, 22	cmpt 5231	. . . . 5 class (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))
24		cgsu 17383	. . . . 5 class Σg
25	6, 23, 24	co 7406	. . . 4 class (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))
26	4, 5, 13, 15, 25	cmpo 7408	. . 3 class (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))))
27	2, 3, 26	cmpt 5231	. 2 class (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))
28	1, 27	wceq 1542	1 wff linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))

This definition is referenced by:  lincop  47043  dflinc2  47045