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

Definition df-linc 41457
 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 ·𝑠. (Contributed by AV, 29-Mar-2019.)
Assertion
Ref Expression
df-linc linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))))
Distinct variable group:   𝑚,𝑠,𝑣,𝑥

Detailed syntax breakdown of Definition df-linc
StepHypRef Expression
1 clinc 41455 . 2 class linC
2 vm . . 3 setvar 𝑚
3 cvv 3191 . . 3 class V
4 vs . . . 4 setvar 𝑠
5 vv . . . 4 setvar 𝑣
62cv 1479 . . . . . . 7 class 𝑚
7 csca 15860 . . . . . . 7 class Scalar
86, 7cfv 5850 . . . . . 6 class (Scalar‘𝑚)
9 cbs 15776 . . . . . 6 class Base
108, 9cfv 5850 . . . . 5 class (Base‘(Scalar‘𝑚))
115cv 1479 . . . . 5 class 𝑣
12 cmap 7803 . . . . 5 class 𝑚
1310, 11, 12co 6605 . . . 4 class ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)
146, 9cfv 5850 . . . . 5 class (Base‘𝑚)
1514cpw 4135 . . . 4 class 𝒫 (Base‘𝑚)
16 vx . . . . . 6 setvar 𝑥
1716cv 1479 . . . . . . . 8 class 𝑥
184cv 1479 . . . . . . . 8 class 𝑠
1917, 18cfv 5850 . . . . . . 7 class (𝑠𝑥)
20 cvsca 15861 . . . . . . . 8 class ·𝑠
216, 20cfv 5850 . . . . . . 7 class ( ·𝑠𝑚)
2219, 17, 21co 6605 . . . . . 6 class ((𝑠𝑥)( ·𝑠𝑚)𝑥)
2316, 11, 22cmpt 4678 . . . . 5 class (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥))
24 cgsu 16017 . . . . 5 class Σg
256, 23, 24co 6605 . . . 4 class (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))
264, 5, 13, 15, 25cmpt2 6607 . . 3 class (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥))))
272, 3, 26cmpt 4678 . 2 class (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))))
281, 27wceq 1480 1 wff linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))))
 Colors of variables: wff setvar class This definition is referenced by:  lincop  41459  dflinc2  41461
 Copyright terms: Public domain W3C validator