---

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

.....wf..... 
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))
⊢ g ∈ B ⟶ A//z.z ∈ Ker(f)
BY
{ ((Assert EquivRel(Point(A);x,y.x = y mod (z.z ∈ Ker(f))) BY
          EAuto 1)
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``vs-point mk-vs vs-quotient vs-add vs-mul`` 0
   THEN Folds ``vs-point vs-add vs-mul`` 0
   THEN EqTypeCD
   THEN Auto
   THEN RepeatFor 2 (UnfoldTopAb 0)
   THEN (Unfold `vs-neg` 0 THEN Fold `vs-subtract` 0)
   THEN (RWO "vs-map-subtract" 0 THENA Auto)
   THEN (RWO "equal-iff-vs-subtract-is-0<" 0 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. EquivRel(Point(A);x,y.x = y mod (z.z ∈ Ker(f)))
10. u : Point(B)
11. v : Point(B)
⊢ (f (g u + v)) = (f g u + g v) ∈ Point(B)

2
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. EquivRel(Point(A);x,y.x = y mod (z.z ∈ Ker(f)))
10. ∀u,v:Point(B).  ((g u + v) = g u + g v ∈ Point(A//z.z ∈ Ker(f)))
11. a : |K|
12. u : Point(B)
⊢ (f (g a * u)) = (f a * g u) ∈ Point(B)

---

Latex:

---

Latex:
.....wf..... 
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)
\mvdash{}  g  \mmember{}  B  {}\mrightarrow{}  A//z.z  \mmember{}  Ker(f)


By

---

Latex:
((Assert  EquivRel(Point(A);x,y.x  =  y  mod  (z.z  \mmember{}  Ker(f)))  BY
                EAuto  1)
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``vs-point  mk-vs  vs-quotient  vs-add  vs-mul``  0
  THEN  Folds  ``vs-point  vs-add  vs-mul``  0
  THEN  EqTypeCD
  THEN  Auto
  THEN  RepeatFor  2  (UnfoldTopAb  0)
  THEN  (Unfold  `vs-neg`  0  THEN  Fold  `vs-subtract`  0)
  THEN  (RWO  "vs-map-subtract"  0  THENA  Auto)
  THEN  (RWO  "equal-iff-vs-subtract-is-0<"  0  THENA  Auto))

---

Home Index