Metamath Proof Explorer

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 = ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clinco 
 |-  LinCo
1 vm 
 |-  m
2 cvv 
 |-  _V
3 vv 
 |-  v
4 cbs 
 |-  Base
5 1 cv 
 |-  m
6 5 4 cfv 
 |-  ( Base ` m )
7 6 cpw 
 |-  ~P ( Base ` m )
8 vc 
 |-  c
9 vs 
 |-  s
10 csca 
 |-  Scalar
11 5 10 cfv 
 |-  ( Scalar ` m )
12 11 4 cfv 
 |-  ( Base ` ( Scalar ` m ) )
13 cmap 
 |-  ^m
14 3 cv 
 |-  v
15 12 14 13 co 
 |-  ( ( Base ` ( Scalar ` m ) ) ^m v )
16 9 cv 
 |-  s
17 cfsupp 
 |-  finSupp
18 c0g 
 |-  0g
19 11 18 cfv 
 |-  ( 0g ` ( Scalar ` m ) )
20 16 19 17 wbr 
 |-  s finSupp ( 0g ` ( Scalar ` m ) )
21 8 cv 
 |-  c
22 clinc 
 |-  linC
23 5 22 cfv 
 |-  ( linC ` m )
24 16 14 23 co 
 |-  ( s ( linC ` m ) v )
25 21 24 wceq 
 |-  c = ( s ( linC ` m ) v )
26 20 25 wa 
 |-  ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) )
27 26 9 15 wrex 
 |-  E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) )
28 27 8 6 crab 
 |-  { c e. ( Base ` m ) | E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) }
29 1 3 2 7 28 cmpo 
 |-  ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )
30 0 29 wceq 
 |-  LinCo = ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )