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	$$⊢\mathrm{linC}=\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{x\in v}{{\sum }_m}\left(s\left(x\right){\cdot }_{m}x\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clinc	$$class\mathrm{linC}$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5		csca	$$class\mathrm{Scalar}$$
6	1	cv	$$setvarm$$
7	6 5	cfv	$$class\mathrm{Scalar}\left(m\right)$$
8	7 4	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}$$
9		cmap	$$class{\uparrow }_{𝑚}$$
10		vv	$$setvarv$$
11	10	cv	$$setvarv$$
12	8 11 9	co	$$class\left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right)$$
13	6 4	cfv	$$class{\mathrm{Base}}_m$$
14	13	cpw	$$class𝒫{\mathrm{Base}}_m$$
15		cgsu	$$class{\Sigma }_{𝑔}$$
16		vx	$$setvarx$$
17	3	cv	$$setvars$$
18	16	cv	$$setvarx$$
19	18 17	cfv	$$classs\left(x\right)$$
20		cvsca	$$class{\cdot }_{𝑠}$$
21	6 20	cfv	$$class{\cdot }_m$$
22	19 18 21	co	$$class\left(s\left(x\right){\cdot }_{m}x\right)$$
23	16 11 22	cmpt	$$class\left(x\in v⟼s\left(x\right){\cdot }_{m}x\right)$$
24	6 23 15	co	$$class\left(\underset{x\in v}{{\sum }_m},\left(s\left(x\right){\cdot }_{m}x\right)\right)$$
25	3 10 12 14 24	cmpo	$$class\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{x\in v}{{\sum }_m}\left(s\left(x\right){\cdot }_{m}x\right)\right)$$
26	1 2 25	cmpt	$$class\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{x\in v}{{\sum }_m}\left(s\left(x\right){\cdot }_{m}x\right)\right)\right)$$
27	0 26	wceq	$$wff\mathrm{linC}=\left(m\in \mathrm{V}⟼\left(s\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^v\right),v\in 𝒫{\mathrm{Base}}_m⟼\underset{x\in v}{{\sum }_m}\left(s\left(x\right){\cdot }_{m}x\right)\right)\right)$$