---

Step * of Lemma mk-vs_wf

∀[K:RngSig]. ∀[V:Type]. ∀[z:V]. ∀[+:V ⟶ V ⟶ V]. ∀[*:|K| ⟶ V ⟶ V].
  Point= V
  zero= z
  x+y= +[x;y]
  a*u= *[a;u] ∈ VectorSpace(K) 
  supposing (∀x,y,z:V.  (+[x;+[y;z]] = +[+[x;y];z] ∈ V))
  ∧ (∀x,y:V.  (+[x;y] = +[y;x] ∈ V))
  ∧ (∀a:|K|. ∀x,y:V.  (*[a;+[x;y]] = +[*[a;x];*[a;y]] ∈ V))
  ∧ (∀x:V. (*[1;x] = x ∈ V))
  ∧ (∀x:V. (*[0;x] = z ∈ V))
  ∧ (∀x:V. ∀a,b:|K|.  (*[a;*[b;x]] = *[a * b;x] ∈ V))
  ∧ (∀x:V. ∀a,b:|K|.  (*[a +K b;x] = +[*[a;x];*[b;x]] ∈ V))
BY
{ (Auto
   THEN Auto
   THEN Unfolds ``mk-vs vector-space`` 0
   THEN RepeatFor 4 ((RecordPlusTypeCD
                      THENL [ Id; ((RepUR ``vs-point`` 0 THEN Try (MemTypeCD)) THEN Reduce 0 THEN Auto)]
                     ))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[V:Type].  \mforall{}[z:V].  \mforall{}[+:V  {}\mrightarrow{}  V  {}\mrightarrow{}  V].  \mforall{}[*:|K|  {}\mrightarrow{}  V  {}\mrightarrow{}  V].
    Point=  V
    zero=  z
    x+y=  +[x;y]
    a*u=  *[a;u]  \mmember{}  VectorSpace(K) 
    supposing  (\mforall{}x,y,z:V.    (+[x;+[y;z]]  =  +[+[x;y];z]))
    \mwedge{}  (\mforall{}x,y:V.    (+[x;y]  =  +[y;x]))
    \mwedge{}  (\mforall{}a:|K|.  \mforall{}x,y:V.    (*[a;+[x;y]]  =  +[*[a;x];*[a;y]]))
    \mwedge{}  (\mforall{}x:V.  (*[1;x]  =  x))
    \mwedge{}  (\mforall{}x:V.  (*[0;x]  =  z))
    \mwedge{}  (\mforall{}x:V.  \mforall{}a,b:|K|.    (*[a;*[b;x]]  =  *[a  *  b;x]))
    \mwedge{}  (\mforall{}x:V.  \mforall{}a,b:|K|.    (*[a  +K  b;x]  =  +[*[a;x];*[b;x]]))


By

---

Latex:
(Auto
  THEN  Auto
  THEN  Unfolds  ``mk-vs  vector-space``  0
  THEN  RepeatFor  4  ((RecordPlusTypeCD
                                        THENL  [  Id
                                                    ;  ((RepUR  ``vs-point``  0  THEN  Try  (MemTypeCD))  THEN  Reduce  0  THEN  Auto)]
                                      ))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index