---

Step * of Lemma vs-lift-neg-bfs

∀[K:CRng]. ∀[S:Type]. ∀[fs:basic-formal-sum(K;S)]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].
  (vs-lift(vs;f;-(fs)) = -K 1 * vs-lift(vs;f;fs) ∈ Point(vs))
BY
{ (Auto
   THEN RepUR ``vs-lift vs-bag-add neg-bfs`` 0
   THEN (RWW "bag-summation-map" 0 THENA Auto)
   THEN Reduce 0
   THEN Fold `vs-bag-add` 0
   THEN RWO "vs-bag-add-mul" 0
   THEN Auto) }

1
1. K : CRng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. vs : VectorSpace(K)
5. f : S ⟶ Point(vs)
⊢ Σ{let k,s = let k,s = p in <-K k, s> in k * f s | p ∈ fs} = Σ{-K 1 * let k,s = p in k * f s | p ∈ fs} ∈ Point(vs)

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[S:Type].  \mforall{}[fs:basic-formal-sum(K;S)].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[f:S  {}\mrightarrow{}  Point(vs)].
    (vs-lift(vs;f;-(fs))  =  -K  1  *  vs-lift(vs;f;fs))


By

---

Latex:
(Auto
  THEN  RepUR  ``vs-lift  vs-bag-add  neg-bfs``  0
  THEN  (RWW  "bag-summation-map"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `vs-bag-add`  0
  THEN  RWO  "vs-bag-add-mul"  0
  THEN  Auto)

---

Home Index