---

Step * of Lemma implies-iso-vs-quotient

No Annotations
∀[K:CRng]. ∀[A:VectorSpace(K)].
  ∀B:VectorSpace(K)
    ((∃f:A ⟶ B. Surj(Point(A);Point(B);f)) ⇒ (∃P:Point(A) ⟶ ℙ. (vs-subspace(K;A;z.P[z]) ∧ B ≅ A//z.P[z])))
BY
{ (Auto
   THEN ExRepD
   THEN D 0 With ⌜λa.a ∈ Ker(f)⌝ 
   THEN Auto
   THEN RepUR ``so_apply`` 0
   THEN Auto
   THEN Unfold `surject` -2
   THEN (Skolemize (-2) `g' THENA Auto)
   THEN D 0 With ⌜g⌝ 
   THEN Auto
   THEN Try (((D 0 With ⌜f⌝  THENA (Auto THEN BLemma `vs-map-quotient-kernel` THEN Auto)) THEN Auto))) }

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

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[K:CRng].  \mforall{}[A:VectorSpace(K)].
    \mforall{}B:VectorSpace(K)
        ((\mexists{}f:A  {}\mrightarrow{}  B.  Surj(Point(A);Point(B);f))
        {}\mRightarrow{}  (\mexists{}P:Point(A)  {}\mrightarrow{}  \mBbbP{}.  (vs-subspace(K;A;z.P[z])  \mwedge{}  B  \mcong{}  A//z.P[z])))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}\mlambda{}a.a  \mmember{}  Ker(f)\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto
  THEN  Unfold  `surject`  -2
  THEN  (Skolemize  (-2)  `g'  THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}g\mkleeneclose{} 
  THEN  Auto
  THEN  Try  (((D  0  With  \mkleeneopen{}f\mkleeneclose{}    THENA  (Auto  THEN  BLemma  `vs-map-quotient-kernel`  THEN  Auto))  THEN  Auto)))

---

Home Index