---

Step * of Lemma ip-triangle-linearity

∀rv:InnerProductSpace. ∀a,b,c:Point.  (Δ(a;b;c) ⇒ (∀t:ℝ. ((r0 < |t|) ⇒ Δ(b + t*a - b;b;c))))
BY
{ (Auto
   THEN ParallelOp -3
   THEN (Assert b + t*a - b - b ≡ t*a - b BY
               (RealVecEqual THEN Auto))
   THEN (RWW "-1 rv-ip-mul rabs-rmul rv-norm-mul" 0⋅ THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. |a - b ⋅ c - b| < (||a - b|| * ||c - b||)
6. t : ℝ
7. r0 < |t|
8. b + t*a - b - b ≡ t*a - b
⊢ (|t| * |a - b ⋅ c - b|) < ((|t| * ||a - b||) * ||c - b||)

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point.    (\mDelta{}(a;b;c)  {}\mRightarrow{}  (\mforall{}t:\mBbbR{}.  ((r0  <  |t|)  {}\mRightarrow{}  \mDelta{}(b  +  t*a  -  b;b;c))))


By

---

Latex:
(Auto
  THEN  ParallelOp  -3
  THEN  (Assert  b  +  t*a  -  b  -  b  \mequiv{}  t*a  -  b  BY
                          (RealVecEqual  THEN  Auto))
  THEN  (RWW  "-1  rv-ip-mul  rabs-rmul  rv-norm-mul"  0\mcdot{}  THENA  Auto))

---

Home Index