---

Step * 1 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 : ℝ
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|))
BY
{ GenConclTerms Auto [⌜|pts|⌝;⌜b * |qts|⌝;⌜-(b) * |rts|⌝;⌜(t 0) * (s 1)⌝;⌜(t 1) * (s 0)⌝]⋅ }

1
1. p : ℝ^2
2. q : ℝ^2
3. r : ℝ^2
4. t : ℝ^2
5. s : ℝ^2
6. b : ℝ
7. (r1 * |pts|) = |pts|
8. v : ℝ
9. |pts| = v ∈ ℝ
10. v1 : ℝ
11. (b * |qts|) = v1 ∈ ℝ
12. v2 : ℝ
13. (-(b) * |rts|) = v2 ∈ ℝ
14. v3 : ℝ
15. ((t 0) * (s 1)) = v3 ∈ ℝ
16. v4 : ℝ
17. ((t 1) * (s 0)) = v4 ∈ ℝ
⊢ (v + ((v1 + ((r1 - b) * (v3 - v4))) + (v2 + ((r1 - -(b)) * (v3 - v4))) + (v4 - v3)) + (v4 - v3)) = (v + v1 + v2)

---

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{}
7.  (r1  *  |pts|)  =  |pts|
\mvdash{}  (|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|))


By

---

Latex:
GenConclTerms  Auto  [\mkleeneopen{}|pts|\mkleeneclose{};\mkleeneopen{}b  *  |qts|\mkleeneclose{};\mkleeneopen{}-(b)  *  |rts|\mkleeneclose{};\mkleeneopen{}(t  0)  *  (s  1)\mkleeneclose{};\mkleeneopen{}(t  1)  *  (s  0)\mkleeneclose{}]\mcdot{}

---

Home Index