---

Step * 2 of Lemma p2-incidence


1. p : ℙ^2
2. v : ℙ^2
3. ((((v 0) * (p 0)) + ((v 1) * (p 1))) - (v 2) * (p 2)) = r0
⊢ v on p
BY
{ (RepUR ``proj-incidence dot-product proj-rev`` 0
   THEN RepeatFor 2 (((RWO "rsum_unroll" (0) THENA Auto) THEN Reduce 0))
   THEN ((RWO "rsum_single" 0 THENA Auto) THEN Reduce 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbP{}\^{}2
2.  v  :  \mBbbP{}\^{}2
3.  ((((v  0)  *  (p  0))  +  ((v  1)  *  (p  1)))  -  (v  2)  *  (p  2))  =  r0
\mvdash{}  v  on  p


By

---

Latex:
(RepUR  ``proj-incidence  dot-product  proj-rev``  0
  THEN  RepeatFor  2  (((RWO  "rsum\_unroll"  (0)  THENA  Auto)  THEN  Reduce  0))
  THEN  ((RWO  "rsum\_single"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  Auto)

---

Home Index