---

Step * 1 of Lemma geo-line-eq_inversion


1. g : EuclideanPlane
2. l : Line
3. m : Line
4. l ≡ m
5. p : Point
6. Colinear(p;fst(m);fst(snd(m))) ∧ p # fst(l)fst(snd(l))
⊢ False
BY
{ ((((D 2 THEN D 3) THEN D 5 THEN D 6) THEN All Reduce⋅) THEN (gSeparatedCasesLSep ⌜x⌝⌜x1⌝⌜y1⌝⋅ THENA Auto)) }

1
1. g : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. x1 : Point
6. y1 : Point
7. m2 : x1 ≠ y1
8. <x, y, l2> ≡ <x1, y1, m2>
9. p : Point
10. Colinear(p;x1;y1) ∧ p # xy
11. x # x1y1
⊢ False

2
1. g : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. x1 : Point
6. y1 : Point
7. m2 : x1 ≠ y1
8. <x, y, l2> ≡ <x1, y1, m2>
9. p : Point
10. Colinear(p;x1;y1)
11. p # xy
12. ¬x # x1y1
13. Colinear(x;x1;y1)
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  l  :  Line
3.  m  :  Line
4.  l  \mequiv{}  m
5.  p  :  Point
6.  Colinear(p;fst(m);fst(snd(m)))  \mwedge{}  p  \#  fst(l)fst(snd(l))
\mvdash{}  False


By

---

Latex:
((((D  2  THEN  D  3)  THEN  D  5  THEN  D  6)  THEN  All  Reduce\mcdot{})
  THEN  (gSeparatedCasesLSep  \mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}x1\mkleeneclose{}\mkleeneopen{}y1\mkleeneclose{}\mcdot{}  THENA  Auto)
  )

---

Home Index