---

Step * 1 of Lemma p2-incidence


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index