---

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

.....antecedent..... 
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 ∈ ℤ)
12. ¬(j = 1 ∈ ℤ)
⊢ (||f x + r(j - 1)*y - x - f x + r(j - 2)*y - x|| = (||f x + r(j)*y - x - f x + r(j - 2)*y - x||/r(2)))
∧ (||f x + r(j - 1)*y - x - f x + r(j)*y - x|| = (||f x + r(j)*y - x - f x + r(j - 2)*y - x||/r(2)))
BY
{ Assert ⌜(||x + r(j - 1)*y - x - x + r(j)*y - x|| = r)
          ∧ (||x + r(j)*y - x - x + r(j - 2)*y - x|| = (r(2) * r))
          ∧ (||x + r(j - 1)*y - x - x + r(j - 2)*y - x|| = r)⌝⋅ }

1
.....assertion..... 
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 ∈ ℤ)
12. ¬(j = 1 ∈ ℤ)
⊢ (||x + r(j - 1)*y - x - x + r(j)*y - x|| = r)
∧ (||x + r(j)*y - x - x + r(j - 2)*y - x|| = (r(2) * r))
∧ (||x + r(j - 1)*y - x - x + r(j - 2)*y - x|| = r)

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 ∈ ℤ)
12. ¬(j = 1 ∈ ℤ)
13. (||x + r(j - 1)*y - x - x + r(j)*y - x|| = r)
∧ (||x + r(j)*y - x - x + r(j - 2)*y - x|| = (r(2) * r))
∧ (||x + r(j - 1)*y - x - x + r(j - 2)*y - x|| = r)
⊢ (||f x + r(j - 1)*y - x - f x + r(j - 2)*y - x|| = (||f x + r(j)*y - x - f x + r(j - 2)*y - x||/r(2)))
∧ (||f x + r(j - 1)*y - x - f x + r(j)*y - x|| = (||f x + r(j)*y - x - f x + r(j - 2)*y - x||/r(2)))

---

Latex:

---

Latex:
.....antecedent..... 
1.  rv  :  InnerProductSpace
2.  f  :  Point  {}\mrightarrow{}  Point
3.  r  :  \{r:\mBbbR{}|  r0  <  r\} 
4.  \mforall{}x,y:Point.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)
5.  \mforall{}x,y:Point.    (((||x  -  y||  =  r)  \mvee{}  (||x  -  y||  =  (r(2)  *  r)))  {}\mRightarrow{}  (||f  x  -  f  y||  =  ||x  -  y||))
6.  x  :  Point
7.  y  :  Point
8.  ||x  -  y||  =  r
9.  j  :  \mBbbN{}
10.  \mforall{}j:\mBbbN{}j.  f  x  +  r(j)*y  -  x  \mequiv{}  f  x  +  r(j)*f  y  -  f  x
11.  \mneg{}(j  =  0)
12.  \mneg{}(j  =  1)
\mvdash{}  (||f  x  +  r(j  -  1)*y  -  x  -  f  x  +  r(j  -  2)*y  -  x||
=  (||f  x  +  r(j)*y  -  x  -  f  x  +  r(j  -  2)*y  -  x||/r(2)))
\mwedge{}  (||f  x  +  r(j  -  1)*y  -  x  -  f  x  +  r(j)*y  -  x||  =  (||f  x  +  r(j)*y  -  x  -  f  x  +  r(j  -  2)*y  -  x||/r(2)))


By

---

Latex:
Assert  \mkleeneopen{}(||x  +  r(j  -  1)*y  -  x  -  x  +  r(j)*y  -  x||  =  r)
                \mwedge{}  (||x  +  r(j)*y  -  x  -  x  +  r(j  -  2)*y  -  x||  =  (r(2)  *  r))
                \mwedge{}  (||x  +  r(j  -  1)*y  -  x  -  x  +  r(j  -  2)*y  -  x||  =  r)\mkleeneclose{}\mcdot{}

---

Home Index