Definition df-linc 45758

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 45756	. 2 class linC
2		vm	. . 3 setvar 𝑚
3		cvv 3433	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5		vv	. . . 4 setvar 𝑣
6	2	cv 1538	. . . . . . 7 class 𝑚
7		csca 16974	. . . . . . 7 class Scalar
8	6, 7	cfv 6437	. . . . . 6 class (Scalar‘𝑚)
9		cbs 16921	. . . . . 6 class Base
10	8, 9	cfv 6437	. . . . 5 class (Base‘(Scalar‘𝑚))
11	5	cv 1538	. . . . 5 class 𝑣
12		cmap 8624	. . . . 5 class ↑m
13	10, 11, 12	co 7284	. . . 4 class ((Base‘(Scalar‘𝑚)) ↑m 𝑣)
14	6, 9	cfv 6437	. . . . 5 class (Base‘𝑚)
15	14	cpw 4534	. . . 4 class 𝒫 (Base‘𝑚)
16		vx	. . . . . 6 setvar 𝑥
17	16	cv 1538	. . . . . . . 8 class 𝑥
18	4	cv 1538	. . . . . . . 8 class 𝑠
19	17, 18	cfv 6437	. . . . . . 7 class (𝑠‘𝑥)
20		cvsca 16975	. . . . . . . 8 class ·𝑠
21	6, 20	cfv 6437	. . . . . . 7 class ( ·𝑠 ‘𝑚)
22	19, 17, 21	co 7284	. . . . . 6 class ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)
23	16, 11, 22	cmpt 5158	. . . . 5 class (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))
24		cgsu 17160	. . . . 5 class Σg
25	6, 23, 24	co 7284	. . . 4 class (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))
26	4, 5, 13, 15, 25	cmpo 7286	. . 3 class (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))))
27	2, 3, 26	cmpt 5158	. 2 class (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))
28	1, 27	wceq 1539	1 wff linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))

This definition is referenced by:  lincop  45760  dflinc2  45762