---

Step * of Lemma rv-mul-rv-sub

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

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

---

Latex:

---

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


By

---

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

---

Home Index