---

Step * of Lemma rv-mul-0

∀[rv:RealVectorSpace]. ∀[a:ℝ].  a*0 ≡ 0
BY
{ (Auto THEN (InstLemma `rv-mul0` [⌜rv⌝;⌜0⌝]⋅ THENA Auto) THEN (RWO  "-1<" 0 THENA Auto)) }

1
1. rv : RealVectorSpace
2. a : ℝ
3. r0*0 ≡ 0
⊢ a*r0*0 ≡ r0*0

---

Latex:

---

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[a:\mBbbR{}].    a*0  \mequiv{}  0


By

---

Latex:
(Auto  THEN  (InstLemma  `rv-mul0`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RWO    "-1<"  0  THENA  Auto))

---

Home Index