---

Step * 1 1 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|
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 ∈ ℝ
18. (v4 - v3) = -(v3 - v4)
19. v5 : ℝ
20. (v3 - v4) = v5 ∈ ℝ
⊢ (v + ((v1 + ((r1 - b) * v5)) + (v2 + ((r1 - -(b)) * v5)) + -(v5)) + -(v5)) = (v + v1 + v2)
BY
{ (nRNorm 0 THEN Auto) }

---

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|
8.  v  :  \mBbbR{}
9.  |pts|  =  v
10.  v1  :  \mBbbR{}
11.  (b  *  |qts|)  =  v1
12.  v2  :  \mBbbR{}
13.  (-(b)  *  |rts|)  =  v2
14.  v3  :  \mBbbR{}
15.  ((t  0)  *  (s  1))  =  v3
16.  v4  :  \mBbbR{}
17.  ((t  1)  *  (s  0))  =  v4
18.  (v4  -  v3)  =  -(v3  -  v4)
19.  v5  :  \mBbbR{}
20.  (v3  -  v4)  =  v5
\mvdash{}  (v  +  ((v1  +  ((r1  -  b)  *  v5))  +  (v2  +  ((r1  -  -(b))  *  v5))  +  -(v5))  +  -(v5))  =  (v  +  v1  +  v2)


By

---

Latex:
(nRNorm  0  THEN  Auto)

---

Home Index