---

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


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)))
13. z : Point(rv)
14. ||z - x|| = (r(n) * r)
15. ||z - y|| = (r(n) * r)
16. a : Point(rv)
17. b : Point(rv)
18. x' : Point(rv)
19. y' : Point(rv)
20. x ≡ z + r(n)*a - z
21. y ≡ z + r(n)*b - z
22. x' ≡ z + r(m)*a - z
23. y' ≡ z + r(m)*b - z
24. ||z - a|| = r
25. ||z - b|| = r
⊢ ||f x - f y|| = ||x - y||
BY
{ ((InstHyp [⌜z⌝;⌜a⌝;⌜n⌝] 6⋅ THENA Auto)
   THEN (FHyp 4 [-7] THENA Auto)
   THEN (RWO "-1<" (-2) THENA Auto)
   THEN Thin (-1)
   THEN (InstHyp [⌜z⌝;⌜b⌝;⌜n⌝] 6⋅ THENA Auto)
   THEN (FHyp 4 [-7] THENA Auto)
   THEN (RWO "-1<" (-2) THENA Auto)
   THEN Thin (-1)
   THEN ((InstHyp [⌜z⌝;⌜a⌝;⌜m⌝] 6⋅ THENA Auto)
         THEN (FHyp 4 [-7] THENA Auto)
         THEN (RWO "-1<" (-2) THENA Auto)
         THEN Thin (-1))
   THEN (InstHyp [⌜z⌝;⌜b⌝;⌜m⌝] 6⋅ THENA Auto)
   THEN (FHyp 4 [-7] THENA Auto)
   THEN (RWO "-1<" (-2) THENA Auto)
   THEN Thin (-1)) }

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. ¬((||x - y|| = r) ∨ (||x - y|| = (r(2) * r)))
13. z : Point(rv)
14. ||z - x|| = (r(n) * r)
15. ||z - y|| = (r(n) * r)
16. a : Point(rv)
17. b : Point(rv)
18. x' : Point(rv)
19. y' : Point(rv)
20. x ≡ z + r(n)*a - z
21. y ≡ z + r(n)*b - z
22. x' ≡ z + r(m)*a - z
23. y' ≡ z + r(m)*b - z
24. ||z - a|| = r
25. ||z - b|| = r
26. f x ≡ f z + r(n)*f a - f z
27. f y ≡ f z + r(n)*f b - f z
28. f x' ≡ f z + r(m)*f a - f z
29. f y' ≡ f z + r(m)*f b - f z
⊢ ||f x - f y|| = ||x - y||

---

Latex:

---

Latex:

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)))
13.  z  :  Point(rv)
14.  ||z  -  x||  =  (r(n)  *  r)
15.  ||z  -  y||  =  (r(n)  *  r)
16.  a  :  Point(rv)
17.  b  :  Point(rv)
18.  x'  :  Point(rv)
19.  y'  :  Point(rv)
20.  x  \mequiv{}  z  +  r(n)*a  -  z
21.  y  \mequiv{}  z  +  r(n)*b  -  z
22.  x'  \mequiv{}  z  +  r(m)*a  -  z
23.  y'  \mequiv{}  z  +  r(m)*b  -  z
24.  ||z  -  a||  =  r
25.  ||z  -  b||  =  r
\mvdash{}  ||f  x  -  f  y||  =  ||x  -  y||


By

---

Latex:
((InstHyp  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  (FHyp  4  [-7]  THENA  Auto)
  THEN  (RWO  "-1<"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (InstHyp  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  (FHyp  4  [-7]  THENA  Auto)
  THEN  (RWO  "-1<"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  ((InstHyp  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
              THEN  (FHyp  4  [-7]  THENA  Auto)
              THEN  (RWO  "-1<"  (-2)  THENA  Auto)
              THEN  Thin  (-1))
  THEN  (InstHyp  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  (FHyp  4  [-7]  THENA  Auto)
  THEN  (RWO  "-1<"  (-2)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index