Definition df-linc

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clinc	⊢ linC
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5		csca	⊢ Scalar
6	1	cv	⊢ 𝑚
7	6 5	cfv	⊢ ( Scalar ‘ 𝑚 )
8	7 4	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑚 ) )
9		cmap	⊢ ↑m
10		vv	⊢ 𝑣
11	10	cv	⊢ 𝑣
12	8 11 9	co	⊢ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 )
13	6 4	cfv	⊢ ( Base ‘ 𝑚 )
14	13	cpw	⊢ 𝒫 ( Base ‘ 𝑚 )
15		cgsu	⊢ Σg
16		vx	⊢ 𝑥
17	3	cv	⊢ 𝑠
18	16	cv	⊢ 𝑥
19	18 17	cfv	⊢ ( 𝑠 ‘ 𝑥 )
20		cvsca	⊢ ·𝑠
21	6 20	cfv	⊢ ( ·𝑠 ‘ 𝑚 )
22	19 18 21	co	⊢ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 )
23	16 11 22	cmpt	⊢ ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) )
24	6 23 15	co	⊢ ( 𝑚 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) )
25	3 10 12 14 24	cmpo	⊢ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) ) )
26	1 2 25	cmpt	⊢ ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) ) ) )
27	0 26	wceq	⊢ linC = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) ) ) )