---

Step * 2 of Lemma vs-quotient_wf

.....subterm..... T:t
4:n
1. K : CRng
2. vs : VectorSpace(K)
3. P : Point(vs) ⟶ ℙ
4. vs-subspace(K;vs;z.P[z])
5. EquivRel(Point(vs);x,y.x = y mod (z.P[z]))
6. Point(vs) ⊆r (x,y:Point(vs)//x = y mod (z.P[z]))
7. k : |K|
8. z : x,y:Point(vs)//x = y mod (z.P[z])
⊢ k * z ∈ x,y:Point(vs)//x = y mod (z.P[z])
BY
{ (DVar `z' THEN EqTypeCD THEN EAuto 1) }

---

Latex:

---

Latex:
.....subterm.....  T:t
4:n
1.  K  :  CRng
2.  vs  :  VectorSpace(K)
3.  P  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
4.  vs-subspace(K;vs;z.P[z])
5.  EquivRel(Point(vs);x,y.x  =  y  mod  (z.P[z]))
6.  Point(vs)  \msubseteq{}r  (x,y:Point(vs)//x  =  y  mod  (z.P[z]))
7.  k  :  |K|
8.  z  :  x,y:Point(vs)//x  =  y  mod  (z.P[z])
\mvdash{}  k  *  z  \mmember{}  x,y:Point(vs)//x  =  y  mod  (z.P[z])


By

---

Latex:
(DVar  `z'  THEN  EqTypeCD  THEN  EAuto  1)

---

Home Index