---

Step * 1 1 1 1 of Lemma vs-map-quotient


1. K : CRng
2. B : VectorSpace(K)
3. ∀x,y:Point(B).  (x = y ∈ Point(B) ⇐⇒ x + -(y) = 0 ∈ Point(B))
⊢ Point(B) ≡ x,y:Point(B)//(x + -(y) = 0 ∈ B."Point")
BY
{ ((Fold `vs-point` 0
    THEN (Assert EquivRel(Point(B);x,y.x + -(y) = 0 ∈ Point(B)) BY
                ((D 0 THEN Auto) THEN D 0 THEN Reduce 0 THEN RWW "3<" 0 THEN Auto))
    )
   THEN RepeatFor 2 (D 0)
   THEN Auto
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  B  :  VectorSpace(K)
3.  \mforall{}x,y:Point(B).    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  x  +  -(y)  =  0)
\mvdash{}  Point(B)  \mequiv{}  x,y:Point(B)//(x  +  -(y)  =  0)


By

---

Latex:
((Fold  `vs-point`  0
    THEN  (Assert  EquivRel(Point(B);x,y.x  +  -(y)  =  0)  BY
                            ((D  0  THEN  Auto)  THEN  D  0  THEN  Reduce  0  THEN  RWW  "3<"  0  THEN  Auto))
    )
  THEN  RepeatFor  2  (D  0)
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index