---

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

.....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)
BY
{ DVar `fs' }

1
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 : Base
9. f1 : Base
10. fs = f1 ∈ pertype(λas,bs. ((as ∈ (|K| × S) List) ∧ (bs ∈ (|K| × S) List) ∧ permutation(|K| × S;as;bs)))
11. fs ∈ (|K| × S) List
12. f1 ∈ (|K| × S) List
13. permutation(|K| × S;fs;f1)
14. as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;S)
15. bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;S)
16. vs : VectorSpace(K)
17. f : S ⟶ Point(vs)
18. IsMonoid(Point(vs);λx,y. x + y;0)
19. Comm(Point(vs);λx,y. x + y)
⊢ vs-lift(vs;f;k +K k' * fs) = vs-lift(vs;f;k * f1) + vs-lift(vs;f;k' * f1) ∈ Point(vs)

---

Latex:

---

Latex:
.....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)
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;k  +K  k'  *  fs)  =  vs-lift(vs;f;k  *  fs)  +  vs-lift(vs;f;k'  *  fs)


By

---

Latex:
DVar  `fs'

---

Home Index