---

Step * 2 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. 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)))
BY
{ (EqTypeCD
   THEN Auto
   THEN RepeatFor 2 (ParallelOp -2)
   THEN ((Unfold `vs-neg` 0 THEN Fold `vs-subtract` 0) THEN Unfold `vs-neg` -2 THEN Fold `vs-subtract` (-2))
   THEN (RWO "vs-map-subtract" (-2) THENA Auto)
   THEN (RWO "equal-iff-vs-subtract-is-0<" (-2) THENA Auto)) }

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. (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)

---

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


By

---

Latex:
(EqTypeCD
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  ((Unfold  `vs-neg`  0  THEN  Fold  `vs-subtract`  0)
              THEN  Unfold  `vs-neg`  -2
              THEN  Fold  `vs-subtract`  (-2))
  THEN  (RWO  "vs-map-subtract"  (-2)  THENA  Auto)
  THEN  (RWO  "equal-iff-vs-subtract-is-0<"  (-2)  THENA  Auto))

---

Home Index