Step
*
2
2
1
of Lemma
implies-isometry-lemma2
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. (||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)))
⇐⇒ f x + r(j - 1)*y - x ≡ (r1/r(2))*f x + r(j - 2)*y - x + f x + r(j)*y - x
⊢ f x + r(j)*y - x ≡ f x + r(j)*f y - f x
BY
{ (D -1 THEN Thin (-1) THEN D -1) }
1
.....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)))
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. f x + r(j - 1)*y - x ≡ (r1/r(2))*f x + r(j - 2)*y - x + f x + r(j)*y - x
⊢ f x + r(j)*y - x ≡ f x + r(j)*f y - f x
Latex:
Latex:
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)
13. (||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)))
\mLeftarrow{}{}\mRightarrow{} f x + r(j - 1)*y - x \mequiv{} (r1/r(2))*f x + r(j - 2)*y - x + f x + r(j)*y - x
\mvdash{} f x + r(j)*y - x \mequiv{} f x + r(j)*f y - f x
By
Latex:
(D -1 THEN Thin (-1) THEN D -1)
Home
Index