---

Step * 1 1 1 of Lemma r2-det-convex3


1. p : ℝ^2
2. q : ℝ^2
3. r : ℝ^2
4. t : ℝ^2
5. s : ℝ^2
6. b : ℝ
⊢ |p + b*q + -(b)*rts| = ((r1 * |pts|) + (b * |qts|) + (-(b) * |rts|))
BY
{ ((Assert (r1 * |pts|) = |pts| BY Auto) THEN (RWO "-1" 0 THENA Auto) THEN (RWW "r2-det-add r2-det-mul" 0 THENA Auto)) }

1
1. p : ℝ^2
2. q : ℝ^2
3. r : ℝ^2
4. t : ℝ^2
5. s : ℝ^2
6. b : ℝ
7. (r1 * |pts|) = |pts|
⊢ (|pts|
+ (((b * |qts|) + ((r1 - b) * (((t 0) * (s 1)) - (t 1) * (s 0))))
  + ((-(b) * |rts|) + ((r1 - -(b)) * (((t 0) * (s 1)) - (t 1) * (s 0))))
  + (((t 1) * (s 0)) - (t 0) * (s 1)))
+ (((t 1) * (s 0)) - (t 0) * (s 1)))
= (|pts| + (b * |qts|) + (-(b) * |rts|))

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}\^{}2
2.  q  :  \mBbbR{}\^{}2
3.  r  :  \mBbbR{}\^{}2
4.  t  :  \mBbbR{}\^{}2
5.  s  :  \mBbbR{}\^{}2
6.  b  :  \mBbbR{}
\mvdash{}  |p  +  b*q  +  -(b)*rts|  =  ((r1  *  |pts|)  +  (b  *  |qts|)  +  (-(b)  *  |rts|))


By

---

Latex:
((Assert  (r1  *  |pts|)  =  |pts|  BY
                Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWW  "r2-det-add  r2-det-mul"  0  THENA  Auto))

---

Home Index