---

Step * 1 2 of Lemma vs-map-quotient


1. K : CRng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. P : Point(A) ⟶ ℙ
5. vs-subspace(K;A;z.P[z])
6. ∀[f:A ⟶ B]. f ∈ A//z.P[z] ⟶ B//z.λ2b.b = 0 ∈ Point(B)[z] supposing ∀a:Point(A). (P[a] ⇒ λ2b.b = 0 ∈ Point(B)[f a])
7. f : A ⟶ B
8. ∀a:Point(A). (P[a] ⇒ ((f a) = 0 ∈ Point(B)))
9. f ∈ A//z.P[z] ⟶ B//z.λ2b.b = 0 ∈ Point(B)[z]
10. Point(B) ≡ Point(B//z.λ2b.b = 0 ∈ Point(B)[z])
⊢ f ∈ A//z.P[z] ⟶ B
BY
{ ((MemTypeHD (-2) THENA Auto)
   THEN Fold `member` (-3)
   THEN (MemTypeCD THENW Auto)
   THEN ((RepeatFor 2 (ParallelOp -2) THEN RepeatFor 2 (ParallelLast)) ORELSE Auto)) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  A  :  VectorSpace(K)
3.  B  :  VectorSpace(K)
4.  P  :  Point(A)  {}\mrightarrow{}  \mBbbP{}
5.  vs-subspace(K;A;z.P[z])
6.  \mforall{}[f:A  {}\mrightarrow{}  B].  f  \mmember{}  A//z.P[z]  {}\mrightarrow{}  B//z.\mlambda{}\msubtwo{}b.b  =  0[z]  supposing  \mforall{}a:Point(A).  (P[a]  {}\mRightarrow{}  \mlambda{}\msubtwo{}b.b  =  0[f  a])
7.  f  :  A  {}\mrightarrow{}  B
8.  \mforall{}a:Point(A).  (P[a]  {}\mRightarrow{}  ((f  a)  =  0))
9.  f  \mmember{}  A//z.P[z]  {}\mrightarrow{}  B//z.\mlambda{}\msubtwo{}b.b  =  0[z]
10.  Point(B)  \mequiv{}  Point(B//z.\mlambda{}\msubtwo{}b.b  =  0[z])
\mvdash{}  f  \mmember{}  A//z.P[z]  {}\mrightarrow{}  B


By

---

Latex:
((MemTypeHD  (-2)  THENA  Auto)
  THEN  Fold  `member`  (-3)
  THEN  (MemTypeCD  THENW  Auto)
  THEN  ((RepeatFor  2  (ParallelOp  -2)  THEN  RepeatFor  2  (ParallelLast))  ORELSE  Auto))

---

Home Index