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 44656
 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‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))))
Distinct variable group:   𝑚,𝑠,𝑣,𝑥

Detailed syntax breakdown of Definition df-linc
StepHypRef Expression
1 clinc 44654 . 2 class linC
2 vm . . 3 setvar 𝑚
3 cvv 3479 . . 3 class V
4 vs . . . 4 setvar 𝑠
5 vv . . . 4 setvar 𝑣
62cv 1537 . . . . . . 7 class 𝑚
7 csca 16557 . . . . . . 7 class Scalar
86, 7cfv 6336 . . . . . 6 class (Scalar‘𝑚)
9 cbs 16472 . . . . . 6 class Base
108, 9cfv 6336 . . . . 5 class (Base‘(Scalar‘𝑚))
115cv 1537 . . . . 5 class 𝑣
12 cmap 8389 . . . . 5 class m
1310, 11, 12co 7138 . . . 4 class ((Base‘(Scalar‘𝑚)) ↑m 𝑣)
146, 9cfv 6336 . . . . 5 class (Base‘𝑚)
1514cpw 4520 . . . 4 class 𝒫 (Base‘𝑚)
16 vx . . . . . 6 setvar 𝑥
1716cv 1537 . . . . . . . 8 class 𝑥
184cv 1537 . . . . . . . 8 class 𝑠
1917, 18cfv 6336 . . . . . . 7 class (𝑠𝑥)
20 cvsca 16558 . . . . . . . 8 class ·𝑠
216, 20cfv 6336 . . . . . . 7 class ( ·𝑠𝑚)
2219, 17, 21co 7138 . . . . . 6 class ((𝑠𝑥)( ·𝑠𝑚)𝑥)
2316, 11, 22cmpt 5127 . . . . 5 class (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥))
24 cgsu 16703 . . . . 5 class Σg
256, 23, 24co 7138 . . . 4 class (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))
264, 5, 13, 15, 25cmpo 7140 . . 3 class (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥))))
272, 3, 26cmpt 5127 . 2 class (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))))
281, 27wceq 1538 1 wff linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥𝑣 ↦ ((𝑠𝑥)( ·𝑠𝑚)𝑥)))))
 Colors of variables: wff setvar class This definition is referenced by:  lincop  44658  dflinc2  44660
 Copyright terms: Public domain W3C validator