---

Step * 1 1 of Lemma ip-triangle-lemma


1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. ||x|| = ||y||
5. r0 < ||x - y||
6. r0 < ||r(-1)*x - y||
7. r0 < ((x^2 - r(2) * x ⋅ y) + y^2)
8. r0 < (x^2 + (r(2) * x ⋅ y) + y^2)
⊢ (x ⋅ y * x ⋅ y) < (x^2 * y^2)
BY
{ ((Assert ||x||^2 = ||y||^2 BY
          (RWO "4" 0 THEN Auto))
   THEN (RWO "rv-norm-squared" (-1) THENA Auto)
   THEN (RWO "-1<" 0 THENA Auto)
   THEN (RWO "-1<" (-2) THENA Auto)
   THEN (RWO "-1<" (-3) THENA Auto)
   THEN (nRNorm (-3) THENA Auto)
   THEN (nRNorm (-2) THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. ||x|| = ||y||
5. r0 < ||x - y||
6. r0 < ||r(-1)*x - y||
7. r0 < ((r(2) * x^2) + (r(-2) * x ⋅ y))
8. r0 < ((r(2) * x^2) + (r(2) * x ⋅ y))
9. x^2 = y^2
⊢ (x ⋅ y * x ⋅ y) < (x^2 * x^2)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point
3.  y  :  Point
4.  ||x||  =  ||y||
5.  r0  <  ||x  -  y||
6.  r0  <  ||r(-1)*x  -  y||
7.  r0  <  ((x\^{}2  -  r(2)  *  x  \mcdot{}  y)  +  y\^{}2)
8.  r0  <  (x\^{}2  +  (r(2)  *  x  \mcdot{}  y)  +  y\^{}2)
\mvdash{}  (x  \mcdot{}  y  *  x  \mcdot{}  y)  <  (x\^{}2  *  y\^{}2)


By

---

Latex:
((Assert  ||x||\^{}2  =  ||y||\^{}2  BY
                (RWO  "4"  0  THEN  Auto))
  THEN  (RWO  "rv-norm-squared"  (-1)  THENA  Auto)
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  (RWO  "-1<"  (-2)  THENA  Auto)
  THEN  (RWO  "-1<"  (-3)  THENA  Auto)
  THEN  (nRNorm  (-3)  THENA  Auto)
  THEN  (nRNorm  (-2)  THENA  Auto))

---

Home Index