---

Step * of Lemma vs-map-kernel-zero

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

1
1. K : Rng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. f : A ⟶ B
5. ∀a:Point(A). (a ∈ Ker(f) ⇐⇒ a = 0 ∈ Point(A))
⊢ Inj(Point(A);Point(B);f)

2
1. K : Rng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. f : A ⟶ B
5. Inj(Point(A);Point(B);f)
6. a : Point(A)
7. a ∈ Ker(f)
⊢ a = 0 ∈ Point(A)

3
1. K : Rng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. f : A ⟶ B
5. Inj(Point(A);Point(B);f)
6. a : Point(A)
7. a = 0 ∈ Point(A)
⊢ a ∈ Ker(f)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index