---

Step * 1 2 of Lemma free-vs-dim-1


1. S : Type
2. s : S
3. K : CRng
4. ∀x,y:S.  (x = y ∈ S)
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
7. ∃!h:one-dim-vs(K) ⟶ vs. ((h 1) = (f s) ∈ Point(vs))
⊢ ∃!h:one-dim-vs(K) ⟶ vs. ∀s:S. ((h 1) = (f s) ∈ Point(vs))
BY
{ RepeatFor 3 (ParallelLast) }

1
1. S : Type
2. s : S
3. K : CRng
4. ∀x,y:S.  (x = y ∈ S)
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
7. h : one-dim-vs(K) ⟶ vs
8. ∀y:one-dim-vs(K) ⟶ vs. (((y 1) = (f s) ∈ Point(vs)) ⇒ (y = h ∈ one-dim-vs(K) ⟶ vs))
9. (h 1) = (f s) ∈ Point(vs)
⊢ ∀s:S. ((h 1) = (f s) ∈ Point(vs))

2
1. S : Type
2. s : S
3. K : CRng
4. ∀x,y:S.  (x = y ∈ S)
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
7. h : one-dim-vs(K) ⟶ vs
8. (h 1) = (f s) ∈ Point(vs)
9. ∀y:one-dim-vs(K) ⟶ vs. (((y 1) = (f s) ∈ Point(vs)) ⇒ (y = h ∈ one-dim-vs(K) ⟶ vs))
⊢ ∀y:one-dim-vs(K) ⟶ vs. ((∀s:S. ((y 1) = (f s) ∈ Point(vs))) ⇒ (y = h ∈ one-dim-vs(K) ⟶ vs))

---

Latex:

---

Latex:

1.  S  :  Type
2.  s  :  S
3.  K  :  CRng
4.  \mforall{}x,y:S.    (x  =  y)
5.  vs  :  VectorSpace(K)
6.  f  :  S  {}\mrightarrow{}  Point(vs)
7.  \mexists{}!h:one-dim-vs(K)  {}\mrightarrow{}  vs.  ((h  1)  =  (f  s))
\mvdash{}  \mexists{}!h:one-dim-vs(K)  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  1)  =  (f  s))


By

---

Latex:
RepeatFor  3  (ParallelLast)

---

Home Index