---

Step * of Lemma free-vs-dim-1

∀S:Type. (S ⇒ (∀K:CRng. free-vs(K;S) ≅ one-dim-vs(K) supposing ∀x,y:S.  (x = y ∈ S)))
BY
{ (Auto
   THEN (InstLemma `free-vs-unique` [⌜S⌝;⌜K⌝;⌜one-dim-vs(K)⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN (D -1 THENM EAuto 1)
   THEN (Subst' Point(one-dim-vs(K)) ~ |K| 0 THENA Computation)
   THEN D 0 With ⌜λx.1⌝ 
   THEN Auto
   THEN Reduce 0
   THEN RenameVar `s' 2) }

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)
⊢ ∃!h:one-dim-vs(K) ⟶ vs. ∀s:S. ((h 1) = (f s) ∈ Point(vs))

---

Latex:

---

Latex:
\mforall{}S:Type.  (S  {}\mRightarrow{}  (\mforall{}K:CRng.  free-vs(K;S)  \mcong{}  one-dim-vs(K)  supposing  \mforall{}x,y:S.    (x  =  y)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `free-vs-unique`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}one-dim-vs(K)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (D  -1  THENM  EAuto  1)
  THEN  (Subst'  Point(one-dim-vs(K))  \msim{}  |K|  0  THENA  Computation)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}x.1\mkleeneclose{} 
  THEN  Auto
  THEN  Reduce  0
  THEN  RenameVar  `s'  2)

---

Home Index