---

Step * 1 2 1 of Lemma vs-lift-unique

.....assertion..... 
1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. f : S ⟶ Point(vs)
5. h : Point(free-vs(K;S)) ⟶ Point(vs)
6. ∀u,v:Point(free-vs(K;S)).  ((h u + v) = h u + h v ∈ Point(vs))
7. ∀a:|K|. ∀u:Point(free-vs(K;S)).  ((h a * u) = a * h u ∈ Point(vs))
8. ∀s:S. ((h <s>) = (f s) ∈ Point(vs))
9. x : Base
10. x1 : Base
11. x = x1 ∈ (a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b))
12. x ∈ basic-formal-sum(K;S)
13. x1 ∈ basic-formal-sum(K;S)
14. bfs-equiv(K;S;x;x1)
15. (h []) = 0 ∈ Point(vs)
⊢ (h x) = vs-lift(vs;f;x) ∈ Point(vs)
BY
{ (ThinVar `x1' THEN (GenConcl ⌜x = fs ∈ basic-formal-sum(K;S)⌝⋅ THENA Auto) THEN ThinVar `x' THEN D -1) }

1
1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. f : S ⟶ Point(vs)
5. h : Point(free-vs(K;S)) ⟶ Point(vs)
6. ∀u,v:Point(free-vs(K;S)).  ((h u + v) = h u + h v ∈ Point(vs))
7. ∀a:|K|. ∀u:Point(free-vs(K;S)).  ((h a * u) = a * h u ∈ Point(vs))
8. ∀s:S. ((h <s>) = (f s) ∈ Point(vs))
9. (h []) = 0 ∈ Point(vs)
10. fs : Base
11. f1 : Base
12. fs = f1 ∈ (as,bs:(|K| × S) List//permutation(|K| × S;as;bs))
13. fs ∈ (|K| × S) List
14. f1 ∈ (|K| × S) List
15. permutation(|K| × S;fs;f1)
⊢ (h fs) = vs-lift(vs;f;f1) ∈ Point(vs)

---

Latex:

---

Latex:
.....assertion..... 
1.  S  :  Type
2.  K  :  CRng
3.  vs  :  VectorSpace(K)
4.  f  :  S  {}\mrightarrow{}  Point(vs)
5.  h  :  Point(free-vs(K;S))  {}\mrightarrow{}  Point(vs)
6.  \mforall{}u,v:Point(free-vs(K;S)).    ((h  u  +  v)  =  h  u  +  h  v)
7.  \mforall{}a:|K|.  \mforall{}u:Point(free-vs(K;S)).    ((h  a  *  u)  =  a  *  h  u)
8.  \mforall{}s:S.  ((h  <s>)  =  (f  s))
9.  x  :  Base
10.  x1  :  Base
11.  x  =  x1
12.  x  \mmember{}  basic-formal-sum(K;S)
13.  x1  \mmember{}  basic-formal-sum(K;S)
14.  bfs-equiv(K;S;x;x1)
15.  (h  [])  =  0
\mvdash{}  (h  x)  =  vs-lift(vs;f;x)


By

---

Latex:
(ThinVar  `x1'  THEN  (GenConcl  \mkleeneopen{}x  =  fs\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `x'  THEN  D  -1)

---

Home Index