---

Step * 2 of Lemma implies-iso-vs-quotient


1. K : CRng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. f : A ⟶ B
5. ∀b:Point(B). ∃a:Point(A). ((f a) = b ∈ Point(B))
6. vs-subspace(K;A;z.λa.a ∈ Ker(f)[z])
7. g : b:Point(B) ⟶ Point(A)
8. ∀b:Point(B). ((f (g b)) = b ∈ Point(B))
9. ∀a:Point(B). ((f (g a)) = a ∈ Point(B))
10. b : Point(A//z.z ∈ Ker(f))
⊢ (g (f b)) = b ∈ Point(A//z.z ∈ Ker(f))
BY
{ ((Assert EquivRel(Point(A);x,y.x = y mod (z.z ∈ Ker(f))) BY
          EAuto 1)
   THEN RepUR ``vs-point mk-vs vs-quotient`` -2
   THEN Folds ``vs-point`` (-2)
   THEN RepUR ``vs-point mk-vs vs-quotient`` 0
   THEN Folds ``vs-point`` 0
   THEN D -2) }

1
1. K : CRng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. f : A ⟶ B
5. ∀b:Point(B). ∃a:Point(A). ((f a) = b ∈ Point(B))
6. vs-subspace(K;A;z.λa.a ∈ Ker(f)[z])
7. g : b:Point(B) ⟶ Point(A)
8. ∀b:Point(B). ((f (g b)) = b ∈ Point(B))
9. ∀a:Point(B). ((f (g a)) = a ∈ Point(B))
10. b : Base
11. b1 : Base
12. b = b1 ∈ (x,y:Point(A)//x = y mod (z.z ∈ Ker(f)))
13. b ∈ Point(A)
14. b1 ∈ Point(A)
15. b = b1 mod (z.z ∈ Ker(f))
16. EquivRel(Point(A);x,y.x = y mod (z.z ∈ Ker(f)))
⊢ (g (f b)) = b1 ∈ (x,y:Point(A)//x = y mod (z.z ∈ Ker(f)))

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  EquivRel(Point(A);x,y.x  =  y  mod  (z.z  \mmember{}  Ker(f)))  BY
                EAuto  1)
  THEN  RepUR  ``vs-point  mk-vs  vs-quotient``  -2
  THEN  Folds  ``vs-point``  (-2)
  THEN  RepUR  ``vs-point  mk-vs  vs-quotient``  0
  THEN  Folds  ``vs-point``  0
  THEN  D  -2)

---

Home Index