Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-linc Structured version   Unicode version

Definition df-linc 31049
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.)
Assertion
Ref Expression
df-linc  |- linC  =  ( m  e.  _V  |->  ( s  e.  ( (
Base `  (Scalar `  m
) )  ^m  v
) ,  v  e. 
~P ( Base `  m
)  |->  ( m  gsumg  ( x  e.  v  |->  ( ( s `  x ) ( .s `  m
) x ) ) ) ) )
Distinct variable group:    m, s, v, x

Detailed syntax breakdown of Definition df-linc
StepHypRef Expression
1 clinc 31047 . 2  class linC
2 vm . . 3  setvar  m
3 cvv 3070 . . 3  class  _V
4 vs . . . 4  setvar  s
5 vv . . . 4  setvar  v
62cv 1369 . . . . . . 7  class  m
7 csca 14345 . . . . . . 7  class Scalar
86, 7cfv 5518 . . . . . 6  class  (Scalar `  m )
9 cbs 14278 . . . . . 6  class  Base
108, 9cfv 5518 . . . . 5  class  ( Base `  (Scalar `  m )
)
115cv 1369 . . . . 5  class  v
12 cmap 7316 . . . . 5  class  ^m
1310, 11, 12co 6192 . . . 4  class  ( (
Base `  (Scalar `  m
) )  ^m  v
)
146, 9cfv 5518 . . . . 5  class  ( Base `  m )
1514cpw 3960 . . . 4  class  ~P ( Base `  m )
16 vx . . . . . 6  setvar  x
1716cv 1369 . . . . . . . 8  class  x
184cv 1369 . . . . . . . 8  class  s
1917, 18cfv 5518 . . . . . . 7  class  ( s `
 x )
20 cvsca 14346 . . . . . . . 8  class  .s
216, 20cfv 5518 . . . . . . 7  class  ( .s
`  m )
2219, 17, 21co 6192 . . . . . 6  class  ( ( s `  x ) ( .s `  m
) x )
2316, 11, 22cmpt 4450 . . . . 5  class  ( x  e.  v  |->  ( ( s `  x ) ( .s `  m
) x ) )
24 cgsu 14483 . . . . 5  class  gsumg
256, 23, 24co 6192 . . . 4  class  ( m 
gsumg  ( x  e.  v  |->  ( ( s `  x ) ( .s
`  m ) x ) ) )
264, 5, 13, 15, 25cmpt2 6194 . . 3  class  ( s  e.  ( ( Base `  (Scalar `  m )
)  ^m  v ) ,  v  e.  ~P ( Base `  m )  |->  ( m  gsumg  ( x  e.  v 
|->  ( ( s `  x ) ( .s
`  m ) x ) ) ) )
272, 3, 26cmpt 4450 . 2  class  ( m  e.  _V  |->  ( s  e.  ( ( Base `  (Scalar `  m )
)  ^m  v ) ,  v  e.  ~P ( Base `  m )  |->  ( m  gsumg  ( x  e.  v 
|->  ( ( s `  x ) ( .s
`  m ) x ) ) ) ) )
281, 27wceq 1370 1  wff linC  =  ( m  e.  _V  |->  ( s  e.  ( (
Base `  (Scalar `  m
) )  ^m  v
) ,  v  e. 
~P ( Base `  m
)  |->  ( m  gsumg  ( x  e.  v  |->  ( ( s `  x ) ( .s `  m
) x ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  lincop  31051  dflinc2  31053
  Copyright terms: Public domain W3C validator