---

Step * 1 2 1 1 1 1 2 of Lemma implies-isometry-lemma5


1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. d : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = d) ∨ (||x - y|| = (r(2) * d))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x - y|| = (r(n) * d/r(m))) ⇒ (||f x - f y|| = ||x - y||))
7. s : ℝ
8. r : ℝ
9. ∃n,m:ℕ+. (s = (r(n)/r(m)))
10. ∃n,m:ℕ+. (r = (r(n)/r(m)))
11. x : Point(rv)
12. y : Point(rv)
13. ||x - y|| ∈ (r * d, s * d)
14. ∃n,m:ℕ+. ((s - r) = (r(n)/r(m)))
15. ∀x,y:Point(rv).  ((||x - y|| < ((s - r) * d)) ⇒ (||f x - f y|| ≤ ((s - r) * d)))
16. ∀x,y:Point(rv).  ((||x - y|| = (s * d)) ⇒ (||f x - f y|| = ||x - y||))
17. r0 < r
18. r0 < (r * d)
19. r0 < ||x - y||
20. r0 < (s * d)
21. ||x + (s * d/||x - y||)*y - x - x|| = (s * d)
⊢ ||x + (s * d/||x - y||)*y - x - y|| < ((s - r) * d)
BY
{ (Assert x + (s * d/||x - y||)*y - x - y ≡ r1 - (s * d/||x - y||)*x - y BY
         ((GenConclTerm ⌜(s * d/||x - y||)⌝⋅ THENA Auto) THEN RealVecEqual THEN Auto)) }

1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. d : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = d) ∨ (||x - y|| = (r(2) * d))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x - y|| = (r(n) * d/r(m))) ⇒ (||f x - f y|| = ||x - y||))
7. s : ℝ
8. r : ℝ
9. ∃n,m:ℕ+. (s = (r(n)/r(m)))
10. ∃n,m:ℕ+. (r = (r(n)/r(m)))
11. x : Point(rv)
12. y : Point(rv)
13. ||x - y|| ∈ (r * d, s * d)
14. ∃n,m:ℕ+. ((s - r) = (r(n)/r(m)))
15. ∀x,y:Point(rv).  ((||x - y|| < ((s - r) * d)) ⇒ (||f x - f y|| ≤ ((s - r) * d)))
16. ∀x,y:Point(rv).  ((||x - y|| = (s * d)) ⇒ (||f x - f y|| = ||x - y||))
17. r0 < r
18. r0 < (r * d)
19. r0 < ||x - y||
20. r0 < (s * d)
21. ||x + (s * d/||x - y||)*y - x - x|| = (s * d)
22. x + (s * d/||x - y||)*y - x - y ≡ r1 - (s * d/||x - y||)*x - y
⊢ ||x + (s * d/||x - y||)*y - x - y|| < ((s - r) * d)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  f  :  Point(rv)  {}\mrightarrow{}  Point(rv)
3.  d  :  \{r:\mBbbR{}|  r0  <  r\} 
4.  \mforall{}x,y:Point(rv).    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)
5.  \mforall{}x,y:Point(rv).    (((||x  -  y||  =  d)  \mvee{}  (||x  -  y||  =  (r(2)  *  d)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
6.  \mforall{}n,m:\mBbbN{}\msupplus{}.  \mforall{}x,y:Point(rv).    ((||x  -  y||  =  (r(n)  *  d/r(m)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
7.  s  :  \mBbbR{}
8.  r  :  \mBbbR{}
9.  \mexists{}n,m:\mBbbN{}\msupplus{}.  (s  =  (r(n)/r(m)))
10.  \mexists{}n,m:\mBbbN{}\msupplus{}.  (r  =  (r(n)/r(m)))
11.  x  :  Point(rv)
12.  y  :  Point(rv)
13.  ||x  -  y||  \mmember{}  (r  *  d,  s  *  d)
14.  \mexists{}n,m:\mBbbN{}\msupplus{}.  ((s  -  r)  =  (r(n)/r(m)))
15.  \mforall{}x,y:Point(rv).    ((||x  -  y||  <  ((s  -  r)  *  d))  {}\mRightarrow{}  (||f  x  -  f  y||  \mleq{}  ((s  -  r)  *  d)))
16.  \mforall{}x,y:Point(rv).    ((||x  -  y||  =  (s  *  d))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
17.  r0  <  r
18.  r0  <  (r  *  d)
19.  r0  <  ||x  -  y||
20.  r0  <  (s  *  d)
21.  ||x  +  (s  *  d/||x  -  y||)*y  -  x  -  x||  =  (s  *  d)
\mvdash{}  ||x  +  (s  *  d/||x  -  y||)*y  -  x  -  y||  <  ((s  -  r)  *  d)


By

---

Latex:
(Assert  x  +  (s  *  d/||x  -  y||)*y  -  x  -  y  \mequiv{}  r1  -  (s  *  d/||x  -  y||)*x  -  y  BY
              ((GenConclTerm  \mkleeneopen{}(s  *  d/||x  -  y||)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  RealVecEqual  THEN  Auto))

---

Home Index