---

Step * 2 1 1 of Lemma vs-map-bag-add


1. K : Rng
2. vs : VectorSpace(K)
3. ws : VectorSpace(K)
4. g : vs ⟶ ws
5. S : Type
6. f : S ⟶ Point(vs)
7. u : S
8. v : S List
9. (g Σ{f[b] | b ∈ v}) = Σ{g f[b] | b ∈ v} ∈ Point(ws)
10. v1 : Point(vs)
11. Σ{f[b] | b ∈ v} = v1 ∈ Point(vs)
⊢ (g Σ{f[b] | b ∈ {u}} + v1) = Σ{g f[b] | b ∈ {u}} + g v1 ∈ Point(ws)
BY
{ Assert ⌜(g Σ{f[b] | b ∈ {u}}) = Σ{g f[b] | b ∈ {u}} ∈ Point(ws)⌝⋅ }

1
.....assertion..... 
1. K : Rng
2. vs : VectorSpace(K)
3. ws : VectorSpace(K)
4. g : vs ⟶ ws
5. S : Type
6. f : S ⟶ Point(vs)
7. u : S
8. v : S List
9. (g Σ{f[b] | b ∈ v}) = Σ{g f[b] | b ∈ v} ∈ Point(ws)
10. v1 : Point(vs)
11. Σ{f[b] | b ∈ v} = v1 ∈ Point(vs)
⊢ (g Σ{f[b] | b ∈ {u}}) = Σ{g f[b] | b ∈ {u}} ∈ Point(ws)

2
1. K : Rng
2. vs : VectorSpace(K)
3. ws : VectorSpace(K)
4. g : vs ⟶ ws
5. S : Type
6. f : S ⟶ Point(vs)
7. u : S
8. v : S List
9. (g Σ{f[b] | b ∈ v}) = Σ{g f[b] | b ∈ v} ∈ Point(ws)
10. v1 : Point(vs)
11. Σ{f[b] | b ∈ v} = v1 ∈ Point(vs)
12. (g Σ{f[b] | b ∈ {u}}) = Σ{g f[b] | b ∈ {u}} ∈ Point(ws)
⊢ (g Σ{f[b] | b ∈ {u}} + v1) = Σ{g f[b] | b ∈ {u}} + g v1 ∈ Point(ws)

---

Latex:

---

Latex:

1.  K  :  Rng
2.  vs  :  VectorSpace(K)
3.  ws  :  VectorSpace(K)
4.  g  :  vs  {}\mrightarrow{}  ws
5.  S  :  Type
6.  f  :  S  {}\mrightarrow{}  Point(vs)
7.  u  :  S
8.  v  :  S  List
9.  (g  \mSigma{}\{f[b]  |  b  \mmember{}  v\})  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  v\}
10.  v1  :  Point(vs)
11.  \mSigma{}\{f[b]  |  b  \mmember{}  v\}  =  v1
\mvdash{}  (g  \mSigma{}\{f[b]  |  b  \mmember{}  \{u\}\}  +  v1)  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  \{u\}\}  +  g  v1


By

---

Latex:
Assert  \mkleeneopen{}(g  \mSigma{}\{f[b]  |  b  \mmember{}  \{u\}\})  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  \{u\}\}\mkleeneclose{}\mcdot{}

---

Home Index