---

Step * 2 1 1 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 : 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. (f b) = (f b1) ∈ Point(B)
16. EquivRel(Point(A);x,y.x = y mod (z.z ∈ Ker(f)))
⊢ (f (g (f b) - b1)) = 0 ∈ Point(B)
BY
{ ((RWO "-2" 0 THEN Auto) THEN (RWO "vs-map-subtract" 0 THENA Auto)) }

---

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  :  Base
11.  b1  :  Base
12.  b  =  b1
13.  b  \mmember{}  Point(A)
14.  b1  \mmember{}  Point(A)
15.  (f  b)  =  (f  b1)
16.  EquivRel(Point(A);x,y.x  =  y  mod  (z.z  \mmember{}  Ker(f)))
\mvdash{}  (f  (g  (f  b)  -  b1))  =  0


By

---

Latex:
((RWO  "-2"  0  THEN  Auto)  THEN  (RWO  "vs-map-subtract"  0  THENA  Auto))

---

Home Index