---

Step * of Lemma vs-lift-bfs-reduce

∀[K:Rng]. ∀[S:Type]. ∀[as,bs:basic-formal-sum(K;S)].
  ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;as) = vs-lift(vs;f;bs) ∈ Point(vs)) 
  supposing bfs-reduce(K;S;as;bs)
BY
{ (Auto
   THEN (Assert IsMonoid(Point(vs);λx,y. x + y;0) BY
               RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto)))
   THEN (Assert Comm(Point(vs);λx,y. x + y) BY
               (D 0 THEN Reduce 0 THEN Auto))
   THEN D 5
   THEN ExRepD
   THEN (RWW "-5 -6 vs-lift-append" 0 THENA Auto)) }

1
1. K : Rng
2. S : Type
3. as : basic-formal-sum(K;S)
4. bs : basic-formal-sum(K;S)
5. s : bag(S)
6. as = (bs + 0 * s) ∈ basic-formal-sum(K;S)
7. vs : VectorSpace(K)
8. f : S ⟶ Point(vs)
9. IsMonoid(Point(vs);λx,y. x + y;0)
10. Comm(Point(vs);λx,y. x + y)
⊢ vs-lift(vs;f;bs) + vs-lift(vs;f;0 * s) = vs-lift(vs;f;bs) ∈ Point(vs)

2
1. K : Rng
2. S : Type
3. as : basic-formal-sum(K;S)
4. bs : basic-formal-sum(K;S)
5. cs : basic-formal-sum(K;S)
6. k : |K|
7. k' : |K|
8. fs : basic-formal-sum(K;S)
9. as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;S)
10. bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;S)
11. vs : VectorSpace(K)
12. f : S ⟶ Point(vs)
13. IsMonoid(Point(vs);λx,y. x + y;0)
14. Comm(Point(vs);λx,y. x + y)
⊢ vs-lift(vs;f;cs) + vs-lift(vs;f;k +K k' * fs)
= vs-lift(vs;f;cs) + vs-lift(vs;f;k * fs) + vs-lift(vs;f;k' * fs)
∈ Point(vs)

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[S:Type].  \mforall{}[as,bs:basic-formal-sum(K;S)].
    \mforall{}[vs:VectorSpace(K)].  \mforall{}[f:S  {}\mrightarrow{}  Point(vs)].    (vs-lift(vs;f;as)  =  vs-lift(vs;f;bs)) 
    supposing  bfs-reduce(K;S;as;bs)


By

---

Latex:
(Auto
  THEN  (Assert  IsMonoid(Point(vs);\mlambda{}x,y.  x  +  y;0)  BY
                          RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))
  THEN  (Assert  Comm(Point(vs);\mlambda{}x,y.  x  +  y)  BY
                          (D  0  THEN  Reduce  0  THEN  Auto))
  THEN  D  5
  THEN  ExRepD
  THEN  (RWW  "-5  -6  vs-lift-append"  0  THENA  Auto))

---

Home Index