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


1. Type
2. CRng
3. VectorSpace(K)
4. S ⟶ Point(V)
5. ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) (f s) ∈ Point(vs))
6. free-vs(K;S) ⟶ V
7. ∀s:S. ((h <s>(i s) ∈ Point(V))
8. V ⟶ free-vs(K;S)
9. ∀s:S. ((f (i s)) = <s> ∈ Point(free-vs(K;S)))
10. h1 free-vs(K;S) ⟶ free-vs(K;S)
11. ∀s:S. ((h1 <s>((λs.<s>s) ∈ Point(free-vs(K;S)))
12. ∀y:free-vs(K;S) ⟶ free-vs(K;S)
      ((∀s:S. ((y <s>((λs.<s>s) ∈ Point(free-vs(K;S))))  (y h1 ∈ free-vs(K;S) ⟶ free-vs(K;S)))
⊢ V ≅ free-vs(K;S)
BY
(InstHyp [⌜λx.x⌝(-1)⋅ THENA (Auto THEN MemTypeCD THEN Reduce THEN Auto)) }

1
1. Type
2. CRng
3. VectorSpace(K)
4. S ⟶ Point(V)
5. ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) (f s) ∈ Point(vs))
6. free-vs(K;S) ⟶ V
7. ∀s:S. ((h <s>(i s) ∈ Point(V))
8. V ⟶ free-vs(K;S)
9. ∀s:S. ((f (i s)) = <s> ∈ Point(free-vs(K;S)))
10. h1 free-vs(K;S) ⟶ free-vs(K;S)
11. ∀s:S. ((h1 <s>((λs.<s>s) ∈ Point(free-vs(K;S)))
12. ∀y:free-vs(K;S) ⟶ free-vs(K;S)
      ((∀s:S. ((y <s>((λs.<s>s) ∈ Point(free-vs(K;S))))  (y h1 ∈ free-vs(K;S) ⟶ free-vs(K;S)))
13. x.x) h1 ∈ free-vs(K;S) ⟶ free-vs(K;S)
⊢ V ≅ free-vs(K;S)


Latex:


Latex:

1.  S  :  Type
2.  K  :  CRng
3.  V  :  VectorSpace(K)
4.  i  :  S  {}\mrightarrow{}  Point(V)
5.  \mforall{}vs:VectorSpace(K).  \mforall{}f:S  {}\mrightarrow{}  Point(vs).    \mexists{}!h:V  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  (i  s))  =  (f  s))
6.  h  :  free-vs(K;S)  {}\mrightarrow{}  V
7.  \mforall{}s:S.  ((h  <s>)  =  (i  s))
8.  f  :  V  {}\mrightarrow{}  free-vs(K;S)
9.  \mforall{}s:S.  ((f  (i  s))  =  <s>)
10.  h1  :  free-vs(K;S)  {}\mrightarrow{}  free-vs(K;S)
11.  \mforall{}s:S.  ((h1  <s>)  =  ((\mlambda{}s.<s>)  s))
12.  \mforall{}y:free-vs(K;S)  {}\mrightarrow{}  free-vs(K;S).  ((\mforall{}s:S.  ((y  <s>)  =  ((\mlambda{}s.<s>)  s)))  {}\mRightarrow{}  (y  =  h1))
\mvdash{}  V  \mcong{}  free-vs(K;S)


By


Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto))




Home Index