---

Step * 2 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 / v]}) = Σ{g f[b] | b ∈ [u / v]} ∈ Point(ws)
BY
{ ((Subst' [u / v] ~ {u} + v 0 THENA Computation) THEN (RWO "vs-bag-add-append" 0 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)
⊢ (g Σ{f[b] | b ∈ {u}} + Σ{f[b] | b ∈ v}) = Σ{g f[b] | b ∈ {u}} + Σ{g f[b] | b ∈ v} ∈ 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  /  v]\})  =  \mSigma{}\{g  f[b]  |  b  \mmember{}  [u  /  v]\}


By

---

Latex:
((Subst'  [u  /  v]  \msim{}  \{u\}  +  v  0  THENA  Computation)  THEN  (RWO  "vs-bag-add-append"  0  THENA  Auto))

---

Home Index