---

Step * 2 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)
⊢ (g Σ{f[b] | b ∈ {u}} + Σ{f[b] | b ∈ v}) = Σ{g f[b] | b ∈ {u}} + Σ{g f[b] | b ∈ v} ∈ Point(ws)
BY
{ ((RWO "-1<" 0⋅ THENA Auto) THEN (GenConclTerm ⌜Σ{f[b] | b ∈ v}⌝⋅ THENA Auto)) }

1
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)

---

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\}
\mvdash{}  (g  \mSigma{}\{f[b]  |  b  \mmember{}  \{u\}\}  +  \mSigma{}\{f[b]  |  b  \mmember{}  v\})  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  \{u\}\}  +  \mSigma{}\{g  f[b]  |  b  \mmember{}  v\}


By

---

Latex:
((RWO  "-1<"  0\mcdot{}  THENA  Auto)  THEN  (GenConclTerm  \mkleeneopen{}\mSigma{}\{f[b]  |  b  \mmember{}  v\}\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index