---

Step * 1 of Lemma vs-quotient_wf

.....subterm..... T:t
3: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. x : x,y:Point(vs)//x = y mod (z.P[z])
8. y : x,y:Point(vs)//x = y mod (z.P[z])
⊢ x + y ∈ x,y:Point(vs)//x = y mod (z.P[z])
BY
{ (DVar `x' THEN DVar `y' THEN EqTypeCD THEN EAuto 1) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3: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.  x  :  x,y:Point(vs)//x  =  y  mod  (z.P[z])
8.  y  :  x,y:Point(vs)//x  =  y  mod  (z.P[z])
\mvdash{}  x  +  y  \mmember{}  x,y:Point(vs)//x  =  y  mod  (z.P[z])


By

---

Latex:
(DVar  `x'  THEN  DVar  `y'  THEN  EqTypeCD  THEN  EAuto  1)

---

Home Index