---

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

∀[K:CRng]. ∀[S:Type]. ∀[fs:basic-formal-sum(K;S)].
  ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;fs) = 0 ∈ Point(vs)) supposing null-formal-sum(K;S;fs)
BY
{ (Auto
   THEN (D -3 THEN ExRepD)
   THEN (Assert vs-lift(vs;f;(b + -(b)) + 0 * ss) = 0 ∈ Point(vs) BY
               (RWW "vs-lift-append vs-lift-neg-bfs vs-lift-zero-bfs" 0 THEN Auto))) }

1
1. K : CRng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. b : bag(|K| × S)
5. ss : bag(S)
6. fs = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
7. vs : VectorSpace(K)
8. f : S ⟶ Point(vs)
⊢ b ∈ formal-sum(K;S)

2
1. K : CRng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. b : bag(|K| × S)
5. ss : bag(S)
6. fs = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
7. vs : VectorSpace(K)
8. f : S ⟶ Point(vs)
⊢ vs-lift(vs;f;b) + -K 1 * vs-lift(vs;f;b) + 0 = 0 ∈ Point(vs)

3
1. K : CRng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. b : bag(|K| × S)
5. ss : bag(S)
6. fs = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
7. vs : VectorSpace(K)
8. f : S ⟶ Point(vs)
9. vs-lift(vs;f;(b + -(b)) + 0 * ss) = 0 ∈ Point(vs)
⊢ vs-lift(vs;f;fs) = 0 ∈ 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)  =  0) 
    supposing  null-formal-sum(K;S;fs)


By

---

Latex:
(Auto
  THEN  (D  -3  THEN  ExRepD)
  THEN  (Assert  vs-lift(vs;f;(b  +  -(b))  +  0  *  ss)  =  0  BY
                          (RWW  "vs-lift-append  vs-lift-neg-bfs  vs-lift-zero-bfs"  0  THEN  Auto)))

---

Home Index