---

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


1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
4. v : ℝ
5. ||x - y|| < (r(2) * v)
6. r0 < ||x - y||
⊢ ∃z:Point(rv). ((||z - x|| = v) ∧ (||z - y|| = v))
BY
{ (((Assert x # y BY
           (BLemma `rv-sep-iff-norm` THEN Auto))
    THEN (Assert x - x + (v/||x - y||)*y - x ≡ (v/||x - y||)*x - y BY
                ((GenConclTerm ⌜(v/||x - y||)⌝⋅ THENA Auto) THEN RealVecEqual THEN Auto))
    THEN (Assert y - y + (v/||x - y||)*x - y ≡ (v/||x - y||)*y - x BY
                ((GenConclTerm ⌜(v/||x - y||)⌝⋅ THENA Auto) THEN RealVecEqual THEN Auto)))
   THEN (Assert r0 < v BY
               (nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
   ) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
4. v : ℝ
5. ||x - y|| < (r(2) * v)
6. r0 < ||x - y||
7. x # y
8. x - x + (v/||x - y||)*y - x ≡ (v/||x - y||)*x - y
9. y - y + (v/||x - y||)*x - y ≡ (v/||x - y||)*y - x
10. r0 < v
⊢ ∃z:Point(rv). ((||z - x|| = v) ∧ (||z - y|| = v))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point(rv)
3.  y  :  Point(rv)
4.  v  :  \mBbbR{}
5.  ||x  -  y||  <  (r(2)  *  v)
6.  r0  <  ||x  -  y||
\mvdash{}  \mexists{}z:Point(rv).  ((||z  -  x||  =  v)  \mwedge{}  (||z  -  y||  =  v))


By

---

Latex:
(((Assert  x  \#  y  BY
                  (BLemma  `rv-sep-iff-norm`  THEN  Auto))
    THEN  (Assert  x  -  x  +  (v/||x  -  y||)*y  -  x  \mequiv{}  (v/||x  -  y||)*x  -  y  BY
                            ((GenConclTerm  \mkleeneopen{}(v/||x  -  y||)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  RealVecEqual  THEN  Auto))
    THEN  (Assert  y  -  y  +  (v/||x  -  y||)*x  -  y  \mequiv{}  (v/||x  -  y||)*y  -  x  BY
                            ((GenConclTerm  \mkleeneopen{}(v/||x  -  y||)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  RealVecEqual  THEN  Auto)))
  THEN  (Assert  r0  <  v  BY
                          (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  )

---

Home Index