---

Step * 2 1 of Lemma unique-one-dim-vs-map


1. K : CRng
2. vs : VectorSpace(K)
3. v : Point(vs)
4. 1 * v = v ∈ Point(vs)
5. y : one-dim-vs(K) ⟶ vs
6. (y 1) = v ∈ Point(vs)
7. x : Point(one-dim-vs(K))
⊢ (y x) = x * v ∈ Point(vs)
BY
{ ((Assert x = x * 1 ∈ Point(one-dim-vs(K)) BY
          (RepUR ``one-dim-vs mk-vs vs-point vs-mul`` 0 THEN Auto))
   THEN (Assert (y x * 1) = x * y 1 ∈ Point(vs) BY
               (RepUR ``vs-point one-dim-vs mk-vs`` -2 THEN Auto THEN DVar `y' THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  vs  :  VectorSpace(K)
3.  v  :  Point(vs)
4.  1  *  v  =  v
5.  y  :  one-dim-vs(K)  {}\mrightarrow{}  vs
6.  (y  1)  =  v
7.  x  :  Point(one-dim-vs(K))
\mvdash{}  (y  x)  =  x  *  v


By

---

Latex:
((Assert  x  =  x  *  1  BY
                (RepUR  ``one-dim-vs  mk-vs  vs-point  vs-mul``  0  THEN  Auto))
  THEN  (Assert  (y  x  *  1)  =  x  *  y  1  BY
                          (RepUR  ``vs-point  one-dim-vs  mk-vs``  -2  THEN  Auto  THEN  DVar  `y'  THEN  Auto))
  THEN  Auto)

---

Home Index