---

Step * 1 of Lemma rv-midpoint-unique


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. ||m - a|| = (||b - a||/r(2))
6. ||m - b|| = (||b - a||/r(2))
⊢ m ≡ (r1/r(2))*a + b
BY
{ ((Assert ||m - b|| = ||b - m|| BY
          Auto)
   THEN (RWO  "-1" (-2) THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-2))
   THEN (GenConcl ⌜m - a = a' ∈ Point(rv)⌝⋅ THENA Auto)
   THEN GenConcl ⌜b - m = b' ∈ Point(rv)⌝⋅
   THEN Auto) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. ||m - b|| = ||b - m||
6. a' : Point(rv)
7. m - a = a' ∈ Point(rv)
8. b' : Point(rv)
9. b - m = b' ∈ Point(rv)
10. ||a'|| = (||b - a||/r(2))
11. ||b'|| = (||b - a||/r(2))
⊢ m ≡ (r1/r(2))*a + b

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  m  :  Point(rv)
5.  ||m  -  a||  =  (||b  -  a||/r(2))
6.  ||m  -  b||  =  (||b  -  a||/r(2))
\mvdash{}  m  \mequiv{}  (r1/r(2))*a  +  b


By

---

Latex:
((Assert  ||m  -  b||  =  ||b  -  m||  BY
                Auto)
  THEN  (RWO    "-1"  (-2)  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-2))
  THEN  (GenConcl  \mkleeneopen{}m  -  a  =  a'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  GenConcl  \mkleeneopen{}b  -  m  =  b'\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index