---

Step * of Lemma rv-mul-sub

∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point].  a - b*x ≡ a*x - b*x
BY
{ (Auto THEN RepUR ``rv-sub rv-minus`` 0 THEN (RWO "rv-mul-mul" 0 THENA Auto)) }

1
1. rv : RealVectorSpace
2. a : ℝ
3. b : ℝ
4. x : Point
⊢ a - b*x ≡ a*x + r(-1) * b*x

---

Latex:

---

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[x:Point].    a  -  b*x  \mequiv{}  a*x  -  b*x


By

---

Latex:
(Auto  THEN  RepUR  ``rv-sub  rv-minus``  0  THEN  (RWO  "rv-mul-mul"  0  THENA  Auto))

---

Home Index