---

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


1. K : CRng
2. B : VectorSpace(K)
⊢ Point(B) ≡ Point(B//z.λ2b.b = 0 ∈ Point(B)[z])
BY
{ ((Assert ∀x,y:Point(B).  (x = y ∈ Point(B) ⇐⇒ x + -(y) = 0 ∈ Point(B)) BY
          (Auto THEN Using [`z',⌜-(y)⌝] (BLemma `vs-add-cancel`)⋅ THEN Auto))
   THEN (Subst' Point(B//z.λ2b.b = 0 ∈ Point(B)[z]) ~ x,y:Point(B)//(x + -(y) = 0 ∈ B."Point") 0
         THENA (Computation THEN RepeatFor 5 (EqCD) THEN Computation)
         )
   ) }

1
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")

---

Latex:

---

Latex:

1.  K  :  CRng
2.  B  :  VectorSpace(K)
\mvdash{}  Point(B)  \mequiv{}  Point(B//z.\mlambda{}\msubtwo{}b.b  =  0[z])


By

---

Latex:
((Assert  \mforall{}x,y:Point(B).    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  x  +  -(y)  =  0)  BY
                (Auto  THEN  Using  [`z',\mkleeneopen{}-(y)\mkleeneclose{}]  (BLemma  `vs-add-cancel`)\mcdot{}  THEN  Auto))
  THEN  (Subst'  Point(B//z.\mlambda{}\msubtwo{}b.b  =  0[z])  \msim{}  x,y:Point(B)//(x  +  -(y)  =  0)  0
              THENA  (Computation  THEN  RepeatFor  5  (EqCD)  THEN  Computation)
              )
  )

---

Home Index