Definition df-linc 47175

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 47173	. 2 class linC
2		vm	. . 3 setvar 𝑚
3		cvv 3474	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5		vv	. . . 4 setvar 𝑣
6	2	cv 1540	. . . . . . 7 class 𝑚
7		csca 17204	. . . . . . 7 class Scalar
8	6, 7	cfv 6543	. . . . . 6 class (Scalar‘𝑚)
9		cbs 17148	. . . . . 6 class Base
10	8, 9	cfv 6543	. . . . 5 class (Base‘(Scalar‘𝑚))
11	5	cv 1540	. . . . 5 class 𝑣
12		cmap 8822	. . . . 5 class ↑m
13	10, 11, 12	co 7411	. . . 4 class ((Base‘(Scalar‘𝑚)) ↑m 𝑣)
14	6, 9	cfv 6543	. . . . 5 class (Base‘𝑚)
15	14	cpw 4602	. . . 4 class 𝒫 (Base‘𝑚)
16		vx	. . . . . 6 setvar 𝑥
17	16	cv 1540	. . . . . . . 8 class 𝑥
18	4	cv 1540	. . . . . . . 8 class 𝑠
19	17, 18	cfv 6543	. . . . . . 7 class (𝑠‘𝑥)
20		cvsca 17205	. . . . . . . 8 class ·𝑠
21	6, 20	cfv 6543	. . . . . . 7 class ( ·𝑠 ‘𝑚)
22	19, 17, 21	co 7411	. . . . . 6 class ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)
23	16, 11, 22	cmpt 5231	. . . . 5 class (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))
24		cgsu 17390	. . . . 5 class Σg
25	6, 23, 24	co 7411	. . . 4 class (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))
26	4, 5, 13, 15, 25	cmpo 7413	. . 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 1541	1 wff linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))

This definition is referenced by:  lincop  47177  dflinc2  47179