---

Step * 1 2 1 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
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))
BY
{ (Auto THEN RWO "-2" 0 THEN Auto THEN EqCD THEN Auto) }

---

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.  h  :  one-dim-vs(K)  {}\mrightarrow{}  vs
8.  \mforall{}y:one-dim-vs(K)  {}\mrightarrow{}  vs.  (((y  1)  =  (f  s))  {}\mRightarrow{}  (y  =  h))
9.  (h  1)  =  (f  s)
\mvdash{}  \mforall{}s:S.  ((h  1)  =  (f  s))


By

---

Latex:
(Auto  THEN  RWO  "-2"  0  THEN  Auto  THEN  EqCD  THEN  Auto)

---

Home Index