---

Step * of Lemma vs-map-0

∀[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B].  ((f 0) = 0 ∈ Point(B))
BY
{ (Auto THEN DVar `f' THEN D -1 THEN InstHyp [⌜0⌝;⌜0⌝] (-1)⋅ THEN Auto) }

1
1. K : Rng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. f : Point(A) ⟶ Point(B)
5. ∀u,v:Point(A).  ((f u + v) = f u + f v ∈ Point(B))
6. ∀a:|K|. ∀u:Point(A).  ((f a * u) = a * f u ∈ Point(B))
7. (f 0 * 0) = 0 * f 0 ∈ Point(B)
⊢ (f 0) = 0 ∈ Point(B)

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[A,B:VectorSpace(K)].  \mforall{}[f:A  {}\mrightarrow{}  B].    ((f  0)  =  0)


By

---

Latex:
(Auto  THEN  DVar  `f'  THEN  D  -1  THEN  InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index