---

Step * of Lemma implies-isometry-lemma2

∀rv:InnerProductSpace. ∀f:Point ⟶ Point. ∀r:{r:ℝ| r0 < r} .
  ((∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y))
  ⇒ (∀x,y:Point.  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||)))
  ⇒ (∀x,y:Point.  ((||x - y|| = r) ⇒ (∀j:ℕ. f x + r(j)*y - x ≡ f x + r(j)*f y - f x))))
BY
{ (CompleteInductionOnNat THEN CaseNat 0 `j') }

1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. r : {r:ℝ| r0 < r} 
4. ∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point.  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
6. x : Point
7. y : Point
8. ||x - y|| = r
9. j : ℕ
10. ∀j:ℕj. f x + r(j)*y - x ≡ f x + r(j)*f y - f x
11. j = 0 ∈ ℤ
⊢ f x + r0*y - x ≡ f x + r0*f y - f x

2
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. r : {r:ℝ| r0 < r} 
4. ∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y)
5. ∀x,y:Point.  (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))
6. x : Point
7. y : Point
8. ||x - y|| = r
9. j : ℕ
10. ∀j:ℕj. f x + r(j)*y - x ≡ f x + r(j)*f y - f x
11. ¬(j = 0 ∈ ℤ)
⊢ f x + r(j)*y - x ≡ f x + r(j)*f y - f x

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}f:Point  {}\mrightarrow{}  Point.  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .
    ((\mforall{}x,y:Point.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y))
    {}\mRightarrow{}  (\mforall{}x,y:Point.    (((||x  -  y||  =  r)  \mvee{}  (||x  -  y||  =  (r(2)  *  r)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||)))
    {}\mRightarrow{}  (\mforall{}x,y:Point.    ((||x  -  y||  =  r)  {}\mRightarrow{}  (\mforall{}j:\mBbbN{}.  f  x  +  r(j)*y  -  x  \mequiv{}  f  x  +  r(j)*f  y  -  f  x))))


By

---

Latex:
(CompleteInductionOnNat  THEN  CaseNat  0  `j')

---

Home Index