---

Step * 2 1 1 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 : 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)
BY
{ Assert ⌜vs-lift(vs;f;k +K k' * fs) = vs-lift(vs;f;k +K k' * f1) ∈ Point(vs)⌝⋅ }

1
.....assertion..... 
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 +K k' * f1) ∈ 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 : 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)
20. vs-lift(vs;f;k +K k' * fs) = vs-lift(vs;f;k +K k' * f1) ∈ Point(vs)
⊢ vs-lift(vs;f;k +K k' * fs) = vs-lift(vs;f;k * f1) + vs-lift(vs;f;k' * f1) ∈ 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  :  Base
9.  f1  :  Base
10.  fs  =  f1
11.  fs  \mmember{}  (|K|  \mtimes{}  S)  List
12.  f1  \mmember{}  (|K|  \mtimes{}  S)  List
13.  permutation(|K|  \mtimes{}  S;fs;f1)
14.  as  =  (cs  +  k  +K  k'  *  fs)
15.  bs  =  (cs  +  k  *  fs  +  k'  *  fs)
16.  vs  :  VectorSpace(K)
17.  f  :  S  {}\mrightarrow{}  Point(vs)
18.  IsMonoid(Point(vs);\mlambda{}x,y.  x  +  y;0)
19.  Comm(Point(vs);\mlambda{}x,y.  x  +  y)
\mvdash{}  vs-lift(vs;f;k  +K  k'  *  fs)  =  vs-lift(vs;f;k  *  f1)  +  vs-lift(vs;f;k'  *  f1)


By

---

Latex:
Assert  \mkleeneopen{}vs-lift(vs;f;k  +K  k'  *  fs)  =  vs-lift(vs;f;k  +K  k'  *  f1)\mkleeneclose{}\mcdot{}

---

Home Index