Definition df-lco

Description: Define the operation constructing the set of all linear combinations for a set of vectors. (Contributed by AV, 31-Mar-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Assertion	df-lco	⊢ LinCo = ( 𝑚 ∈ V , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑐 ∈ ( Base ‘ 𝑚 ) ∣ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clinco	⊢ LinCo
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cbs	⊢ Base
5	1	cv	⊢ 𝑚
6	5 4	cfv	⊢ ( Base ‘ 𝑚 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑚 )
8		vc	⊢ 𝑐
9		vs	⊢ 𝑠
10		csca	⊢ Scalar
11	5 10	cfv	⊢ ( Scalar ‘ 𝑚 )
12	11 4	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑚 ) )
13		cmap	⊢ ↑m
14	3	cv	⊢ 𝑣
15	12 14 13	co	⊢ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 )
16	9	cv	⊢ 𝑠
17		cfsupp	⊢ finSupp
18		c0g	⊢ 0g
19	11 18	cfv	⊢ ( 0g ‘ ( Scalar ‘ 𝑚 ) )
20	16 19 17	wbr	⊢ 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) )
21	8	cv	⊢ 𝑐
22		clinc	⊢ linC
23	5 22	cfv	⊢ ( linC ‘ 𝑚 )
24	16 14 23	co	⊢ ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 )
25	21 24	wceq	⊢ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 )
26	20 25	wa	⊢ ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) )
27	26 9 15	wrex	⊢ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) )
28	27 8 6	crab	⊢ { 𝑐 ∈ ( Base ‘ 𝑚 ) ∣ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) }
29	1 3 2 7 28	cmpo	⊢ ( 𝑚 ∈ V , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑐 ∈ ( Base ‘ 𝑚 ) ∣ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) } )
30	0 29	wceq	⊢ LinCo = ( 𝑚 ∈ V , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑐 ∈ ( Base ‘ 𝑚 ) ∣ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) } )