---

Step * of Lemma p2J_wf

∀[a,b:ℙ^2].  p2J(a;b) ∈ ℙ^2 supposing a ≠ b
BY
{ (Auto
   THEN (Assert p2J(a;b) ∈ ℝ^3 BY
               ProveWfLemma)
   THEN (FLemma `proj-sep-implies` [-2] THENA Auto)
   THEN ExRepD
   THEN MemTypeCD
   THEN Auto
   THEN All Reduce) }

1
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. p2J(a;b) ∈ ℝ^3
5. i : ℕ3
6. j : ℕ3
7. (a i) * (b j) ≠ (a j) * (b i)
⊢ ∃k:ℕ3. p2J(a;b) k ≠ r0

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbP{}\^{}2].    p2J(a;b)  \mmember{}  \mBbbP{}\^{}2  supposing  a  \mneq{}  b


By

---

Latex:
(Auto
  THEN  (Assert  p2J(a;b)  \mmember{}  \mBbbR{}\^{}3  BY
                          ProveWfLemma)
  THEN  (FLemma  `proj-sep-implies`  [-2]  THENA  Auto)
  THEN  ExRepD
  THEN  MemTypeCD
  THEN  Auto
  THEN  All  Reduce)

---

Home Index