---

Step * 2 of Lemma vs-lift-bfs-reduce


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)
BY
{ EqCDA }

1
.....subterm..... T:t
3:n
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;k +K k' * fs) = vs-lift(vs;f;k * fs) + vs-lift(vs;f;k' * fs) ∈ Point(vs)

---

Latex:

---

Latex:

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)
10.  bs  =  (cs  +  k  *  fs  +  k'  *  fs)
11.  vs  :  VectorSpace(K)
12.  f  :  S  {}\mrightarrow{}  Point(vs)
13.  IsMonoid(Point(vs);\mlambda{}x,y.  x  +  y;0)
14.  Comm(Point(vs);\mlambda{}x,y.  x  +  y)
\mvdash{}  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)


By

---

Latex:
EqCDA

---

Home Index