---

Step * 1 of Lemma eq-0-in-vs-quotient

.....antecedent..... 
1. K : CRng
2. vs : VectorSpace(K)
3. P : Point(vs) ⟶ ℙ
4. vs-subspace(K;vs;z.P[z])
5. z : Point(vs)
6. P[z]
⊢ z = 0 mod (z.P[z])
BY
{ (RepUR ``eq-mod-subspace`` 0 THEN Subst' z + -(0) = z ∈ Point(vs) 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  K  :  CRng
2.  vs  :  VectorSpace(K)
3.  P  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
4.  vs-subspace(K;vs;z.P[z])
5.  z  :  Point(vs)
6.  P[z]
\mvdash{}  z  =  0  mod  (z.P[z])


By

---

Latex:
(RepUR  ``eq-mod-subspace``  0  THEN  Subst'  z  +  -(0)  =  z  0  THEN  Auto)

---

Home Index