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 32742
 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 , Scalar s and a scalar multiplication . (Contributed by AV, 29-Mar-2019.)
Assertion
Ref Expression
df-linc linC Scalar g
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-linc
StepHypRef Expression
1 clinc 32740 . 2 linC
2 vm . . 3
3 cvv 3095 . . 3
4 vs . . . 4
5 vv . . . 4
62cv 1382 . . . . . . 7
7 csca 14577 . . . . . . 7 Scalar
86, 7cfv 5578 . . . . . 6 Scalar
9 cbs 14509 . . . . . 6
108, 9cfv 5578 . . . . 5 Scalar
115cv 1382 . . . . 5
12 cmap 7422 . . . . 5
1310, 11, 12co 6281 . . . 4 Scalar
146, 9cfv 5578 . . . . 5
1514cpw 3997 . . . 4
16 vx . . . . . 6
1716cv 1382 . . . . . . . 8
184cv 1382 . . . . . . . 8
1917, 18cfv 5578 . . . . . . 7
20 cvsca 14578 . . . . . . . 8
216, 20cfv 5578 . . . . . . 7
2219, 17, 21co 6281 . . . . . 6
2316, 11, 22cmpt 4495 . . . . 5
24 cgsu 14715 . . . . 5 g
256, 23, 24co 6281 . . . 4 g
264, 5, 13, 15, 25cmpt2 6283 . . 3 Scalar g
272, 3, 26cmpt 4495 . 2 Scalar g
281, 27wceq 1383 1 linC Scalar g
 Colors of variables: wff setvar class This definition is referenced by:  lincop  32744  dflinc2  32746
 Copyright terms: Public domain W3C validator