---

Step * 2 of Lemma rv-midpoint-unique


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. m ≡ (r1/r(2))*a + b
⊢ ||m - a|| = (||b - a||/r(2))
BY
{ ((RWO "-1" 0 THENA Auto)
   THEN (Assert (||b - a||/r(2)) = ||(r1/r(2))*b - a|| BY
               ((RWO "rv-norm-mul" 0 THENA Auto)
                THEN (RWO "rabs-of-nonneg" 0 THENA Auto)
                THEN nRMul ⌜r(2)⌝ 0⋅
                THEN Auto))
   THEN ((RWO "-1" 0 THENM BLemma `rv-norm_functionality`) THENA Auto)
   THEN RepUR ``rv-sub rv-minus`` 0
   THEN (RWW "rv-mul-linear rv-mul-mul" 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. m ≡ (r1/r(2))*a + b
6. (||b - a||/r(2)) = ||(r1/r(2))*b - a||
⊢ (r1/r(2))*a + (r1/r(2))*b + r(-1)*a ≡ (r1/r(2))*b + (r1/r(2)) * r(-1)*a

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)
  THEN  (Assert  (||b  -  a||/r(2))  =  ||(r1/r(2))*b  -  a||  BY
                          ((RWO  "rv-norm-mul"  0  THENA  Auto)
                            THEN  (RWO  "rabs-of-nonneg"  0  THENA  Auto)
                            THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto))
  THEN  ((RWO  "-1"  0  THENM  BLemma  `rv-norm\_functionality`)  THENA  Auto)
  THEN  RepUR  ``rv-sub  rv-minus``  0
  THEN  (RWW  "rv-mul-linear  rv-mul-mul"  0  THENA  Auto))

---

Home Index