---

Step * of Lemma vs-iso-iff-kernel-0

∀[K:Rng]. ∀[A,B:VectorSpace(K)].
  (A ≅ B ⇐⇒ ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f) ⇐⇒ a = 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f)))
BY
{ Auto }

1
1. [K] : Rng
2. [A] : VectorSpace(K)
3. [B] : VectorSpace(K)
4. A ≅ B
⊢ ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f) ⇐⇒ a = 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f))

2
1. [K] : Rng
2. [A] : VectorSpace(K)
3. [B] : VectorSpace(K)
4. ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f) ⇐⇒ a = 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f))
⊢ A ≅ B

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[A,B:VectorSpace(K)].
    (A  \mcong{}  B  \mLeftarrow{}{}\mRightarrow{}  \mexists{}f:A  {}\mrightarrow{}  B.  ((\mforall{}a:Point(A).  (a  \mmember{}  Ker(f)  \mLeftarrow{}{}\mRightarrow{}  a  =  0))  \mwedge{}  Surj(Point(A);Point(B);f)))


By

---

Latex:
Auto

---

Home Index