---

Step * of Lemma vs-zero-mul

∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[k:|K|].  (k * 0 = 0 ∈ Point(vs))
BY
{ (Auto THEN (Assert k * 0 = k * 0 + k * 0 ∈ Point(vs) BY (RWW "vs-mul-linear< vs-zero-add" 0 THEN Auto))) }

1
1. K : Rng
2. vs : VectorSpace(K)
3. k : |K|
4. k * 0 = k * 0 + k * 0 ∈ Point(vs)
⊢ k * 0 = 0 ∈ Point(vs)

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[k:|K|].    (k  *  0  =  0)


By

---

Latex:
(Auto  THEN  (Assert  k  *  0  =  k  *  0  +  k  *  0  BY  (RWW  "vs-mul-linear<  vs-zero-add"  0  THEN  Auto)))

---

Home Index