---

Step * 1 1 of Lemma implies-isometry-lemma3

.....assertion..... 
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. r : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀x,y:Point(rv).  ((||x - y|| = r) ⇒ (∀j:ℕ. f x + r(j)*y - x ≡ f x + r(j)*f y - f x))
7. n : ℕ+
8. m : ℕ+
9. x : Point(rv)
10. y : Point(rv)
11. ||x - y|| = (r(n) * r/r(m))
12. ¬((||x - y|| = r) ∨ (||x - y|| = (r(2) * r)))
⊢ ∃z:Point(rv). ((||z - x|| = (r(n) * r)) ∧ (||z - y|| = (r(n) * r)))
BY
{ (Thin (-1)
   THEN (Assert r0 < (r(n) * r) BY
               EAuto 2)
   THEN (Assert (r(n) * r) = (r(m) * (r(n) * r/r(m))) BY
               ((GenConclTerm ⌜r(n) * r⌝⋅ THENA Auto) THEN nRNorm 0 THEN Auto))
   THEN (Assert r0 < (r(n) * r/r(m)) BY
               (nRMul ⌜r(m)⌝ 0⋅ THEN Auto))) }

1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. r : {r:ℝ| r0 < r} 
4. ∀x,y:Point(rv).  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point(rv).  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
6. ∀x,y:Point(rv).  ((||x - y|| = r) ⇒ (∀j:ℕ. f x + r(j)*y - x ≡ f x + r(j)*f y - f x))
7. n : ℕ+
8. m : ℕ+
9. x : Point(rv)
10. y : Point(rv)
11. ||x - y|| = (r(n) * r/r(m))
12. r0 < (r(n) * r)
13. (r(n) * r) = (r(m) * (r(n) * r/r(m)))
14. r0 < (r(n) * r/r(m))
⊢ ∃z:Point(rv). ((||z - x|| = (r(n) * r)) ∧ (||z - y|| = (r(n) * r)))

---

Latex:

---

Latex:
.....assertion..... 
1.  rv  :  InnerProductSpace
2.  f  :  Point(rv)  {}\mrightarrow{}  Point(rv)
3.  r  :  \{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||  =  r)  \mvee{}  (||x  -  y||  =  (r(2)  *  r)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
6.  \mforall{}x,y:Point(rv).    ((||x  -  y||  =  r)  {}\mRightarrow{}  (\mforall{}j:\mBbbN{}.  f  x  +  r(j)*y  -  x  \mequiv{}  f  x  +  r(j)*f  y  -  f  x))
7.  n  :  \mBbbN{}\msupplus{}
8.  m  :  \mBbbN{}\msupplus{}
9.  x  :  Point(rv)
10.  y  :  Point(rv)
11.  ||x  -  y||  =  (r(n)  *  r/r(m))
12.  \mneg{}((||x  -  y||  =  r)  \mvee{}  (||x  -  y||  =  (r(2)  *  r)))
\mvdash{}  \mexists{}z:Point(rv).  ((||z  -  x||  =  (r(n)  *  r))  \mwedge{}  (||z  -  y||  =  (r(n)  *  r)))


By

---

Latex:
(Thin  (-1)
  THEN  (Assert  r0  <  (r(n)  *  r)  BY
                          EAuto  2)
  THEN  (Assert  (r(n)  *  r)  =  (r(m)  *  (r(n)  *  r/r(m)))  BY
                          ((GenConclTerm  \mkleeneopen{}r(n)  *  r\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  nRNorm  0  THEN  Auto))
  THEN  (Assert  r0  <  (r(n)  *  r/r(m))  BY
                          (nRMul  \mkleeneopen{}r(m)\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index