---

Step * 1 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]
⊢ f ∈ A//z.P[z] ⟶ B
BY
{ Assert ⌜Point(B) ≡ Point(B//z.λ2b.b = 0 ∈ Point(B)[z])⌝⋅ }

1
.....assertion..... 
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]
⊢ Point(B) ≡ Point(B//z.λ2b.b = 0 ∈ Point(B)[z])

2
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

---

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]
\mvdash{}  f  \mmember{}  A//z.P[z]  {}\mrightarrow{}  B


By

---

Latex:
Assert  \mkleeneopen{}Point(B)  \mequiv{}  Point(B//z.\mlambda{}\msubtwo{}b.b  =  0[z])\mkleeneclose{}\mcdot{}

---

Home Index