---

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

.....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)
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' * f1) = vs-lift(vs;f;k * f1) + vs-lift(vs;f;k' * f1) ∈ Point(vs)
BY
{ ((GenConcl ⌜f1 = L ∈ ((|K| × S) List)⌝⋅ THENA Auto) THEN All Thin) }

1
1. K : Rng
2. S : Type
3. k : |K|
4. k' : |K|
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
7. L : (|K| × S) List
⊢ vs-lift(vs;f;k +K k' * L) = vs-lift(vs;f;k * L) + vs-lift(vs;f;k' * L) ∈ Point(vs)

---

Latex:

---

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


By

---

Latex:
((GenConcl  \mkleeneopen{}f1  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index