---

Step * of Lemma vs-lift-formal-sum-mul

∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[S:Type]. ∀[f:S ⟶ Point(vs)]. ∀[k:|K|]. ∀[x:basic-formal-sum(K;S)].
  (vs-lift(vs;f;k * x) = k * vs-lift(vs;f;x) ∈ Point(vs))
BY
{ (Auto
   THEN All (RepUR ``basic-formal-sum formal-sum-mul vs-lift``)
   THEN (RWO "vs-bag-add-mul" 0 THENA Auto)
   THEN Unfold `vs-bag-add` 0
   THEN (RWO "bag-summation-map" 0 THENA Auto)
   THEN EqCDA
   THEN ((RepeatFor 2 (D 0) THEN Reduce 0 THEN Complete (Auto)) ORELSE (D -1 THEN Reduce 0 THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``basic-formal-sum  formal-sum-mul  vs-lift``)
  THEN  (RWO  "vs-bag-add-mul"  0  THENA  Auto)
  THEN  Unfold  `vs-bag-add`  0
  THEN  (RWO  "bag-summation-map"  0  THENA  Auto)
  THEN  EqCDA
  THEN  ((RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Complete  (Auto))
  ORELSE  (D  -1  THEN  Reduce  0  THEN  Auto)
  ))

---

Home Index