---

Step * 1 1 2 1 of Lemma r2-dot-product-eq-0-iff-perp


1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. y⋅x = r0
5. ||r2-perp(x)|| = r1
6. r0 < ||r2-perp(x)||
7. i : ℤ
8. r0 ≠ (-(x 1)/||x||)
9. i = 0 ∈ ℤ
10. i1 : ℤ
11. i1 = 1 ∈ ℤ
12. v : ℝ
13. (-(x 1)/||x||) = v ∈ ℝ
14. v ≠ r0
⊢ -((x 1) * (y 1)) = ((x 0) * (y 0))
BY
{ (Assert y⋅x = (((x 0) * (y 0)) + ((x 1) * (y 1))) BY
         (RepUR ``dot-product`` 0
          THEN (RWO "rsum-split-first" 0 THENA Auto)
          THEN Reduce 0
          THEN RWO "rsum-single" 0
          THEN Reduce 0
          THEN Auto)) }

1
1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. y⋅x = r0
5. ||r2-perp(x)|| = r1
6. r0 < ||r2-perp(x)||
7. i : ℤ
8. r0 ≠ (-(x 1)/||x||)
9. i = 0 ∈ ℤ
10. i1 : ℤ
11. i1 = 1 ∈ ℤ
12. v : ℝ
13. (-(x 1)/||x||) = v ∈ ℝ
14. v ≠ r0
15. y⋅x = (((x 0) * (y 0)) + ((x 1) * (y 1)))
⊢ -((x 1) * (y 1)) = ((x 0) * (y 0))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}\^{}2
2.  r0  <  ||x||
3.  y  :  \mBbbR{}\^{}2
4.  y\mcdot{}x  =  r0
5.  ||r2-perp(x)||  =  r1
6.  r0  <  ||r2-perp(x)||
7.  i  :  \mBbbZ{}
8.  r0  \mneq{}  (-(x  1)/||x||)
9.  i  =  0
10.  i1  :  \mBbbZ{}
11.  i1  =  1
12.  v  :  \mBbbR{}
13.  (-(x  1)/||x||)  =  v
14.  v  \mneq{}  r0
\mvdash{}  -((x  1)  *  (y  1))  =  ((x  0)  *  (y  0))


By

---

Latex:
(Assert  y\mcdot{}x  =  (((x  0)  *  (y  0))  +  ((x  1)  *  (y  1)))  BY
              (RepUR  ``dot-product``  0
                THEN  (RWO  "rsum-split-first"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  RWO  "rsum-single"  0
                THEN  Reduce  0
                THEN  Auto))

---

Home Index