---

Step * of Lemma p2-incidence

∀[p,v:ℙ^2].  uiff(v on p;((((v 0) * (p 0)) + ((v 1) * (p 1))) - (v 2) * (p 2)) = r0)
BY
{ Auto }

1
1. p : ℙ^2
2. v : ℙ^2
3. v on p
⊢ ((((v 0) * (p 0)) + ((v 1) * (p 1))) - (v 2) * (p 2)) = r0

2
1. p : ℙ^2
2. v : ℙ^2
3. ((((v 0) * (p 0)) + ((v 1) * (p 1))) - (v 2) * (p 2)) = r0
⊢ v on p

---

Latex:

---

Latex:
\mforall{}[p,v:\mBbbP{}\^{}2].    uiff(v  on  p;((((v  0)  *  (p  0))  +  ((v  1)  *  (p  1)))  -  (v  2)  *  (p  2))  =  r0)


By

---

Latex:
Auto

---

Home Index