---

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

∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].
  ∀z:Point(vs). z = 0 ∈ Point(vs//z.P[z]) supposing ↓P[z] supposing vs-subspace(K;vs;z.P[z])
BY
{ (Auto THEN RepUR ``vs-quotient vs-0 vs-point mk-vs`` 0 THEN Folds ``vs-point vs-0`` 0 THEN EqTypeCD THEN EAuto 1) }

1
.....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])

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[P:Point(vs)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}z:Point(vs).  z  =  0  supposing  \mdownarrow{}P[z]  supposing  vs-subspace(K;vs;z.P[z])


By

---

Latex:
(Auto
  THEN  RepUR  ``vs-quotient  vs-0  vs-point  mk-vs``  0
  THEN  Folds  ``vs-point  vs-0``  0
  THEN  EqTypeCD
  THEN  EAuto  1)

---

Home Index