Metamath Proof Explorer

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 = ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clinc 
 |-  linC
1 vm 
 |-  m
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cbs 
 |-  Base
5 csca 
 |-  Scalar
6 1 cv 
 |-  m
7 6 5 cfv 
 |-  ( Scalar ` m )
8 7 4 cfv 
 |-  ( Base ` ( Scalar ` m ) )
9 cmap 
 |-  ^m
10 vv 
 |-  v
11 10 cv 
 |-  v
12 8 11 9 co 
 |-  ( ( Base ` ( Scalar ` m ) ) ^m v )
13 6 4 cfv 
 |-  ( Base ` m )
14 13 cpw 
 |-  ~P ( Base ` m )
15 cgsu 
 |-  gsum
16 vx 
 |-  x
17 3 cv 
 |-  s
18 16 cv 
 |-  x
19 18 17 cfv 
 |-  ( s ` x )
20 cvsca 
 |-  .s
21 6 20 cfv 
 |-  ( .s ` m )
22 19 18 21 co 
 |-  ( ( s ` x ) ( .s ` m ) x )
23 16 11 22 cmpt 
 |-  ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) )
24 6 23 15 co 
 |-  ( m gsum ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) )
25 3 10 12 14 24 cmpo 
 |-  ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) )
26 1 2 25 cmpt 
 |-  ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )
27 0 26 wceq 
 |-  linC = ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )