---

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

.....subterm..... T:t
2:n
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 : Point(free-vs(K;S))
10. {} ∈ Point(free-vs(K;S))
11. (h 0 * {}) = 0 * h {} ∈ Point(vs)
⊢ (h {}) = (h 0 * {}) ∈ Point(vs)
BY
{ (EqCDA THEN SubsumeC ⌜basic-formal-sum(K;S)⌝⋅ THEN Auto THEN Unfold `basic-formal-sum` 0 THEN Auto) }

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. x : Point(free-vs(K;S))
10. {} ∈ Point(free-vs(K;S))
11. (h 0 * {}) = 0 * h {} ∈ Point(vs)
12. {} = 0 * {} ∈ basic-formal-sum(K;S)
⊢ bag(|K| × S) ⊆r Point(free-vs(K;S))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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  :  Point(free-vs(K;S))
10.  \{\}  \mmember{}  Point(free-vs(K;S))
11.  (h  0  *  \{\})  =  0  *  h  \{\}
\mvdash{}  (h  \{\})  =  (h  0  *  \{\})


By

---

Latex:
(EqCDA  THEN  SubsumeC  \mkleeneopen{}basic-formal-sum(K;S)\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Unfold  `basic-formal-sum`  0  THEN  Auto)

---

Home Index