---

Step * of Lemma ip-dist-between-1

∀[rv:InnerProductSpace]. ∀[t:ℝ]. ∀[a,c:Point].  (||a - t*a + r1 - t*c|| = (|r1 - t| * ||a - c||))
BY
{ (Auto
   THEN (RWO "rv-norm-mul<" 0 THENA Auto)
   THEN (BLemma `rv-norm_functionality` THENA Auto)
   THEN RealVecEqual
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[t:\mBbbR{}].  \mforall{}[a,c:Point].    (||a  -  t*a  +  r1  -  t*c||  =  (|r1  -  t|  *  ||a  -  c||))


By

---

Latex:
(Auto
  THEN  (RWO  "rv-norm-mul<"  0  THENA  Auto)
  THEN  (BLemma  `rv-norm\_functionality`  THENA  Auto)
  THEN  RealVecEqual
  THEN  Auto)

---

Home Index