---

Step * 1 1 1 of Lemma geo-intersect-unique


1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. ∃z:Point. (z I l ∧ z # m)
12. ∀a,b,c,d,p,q:Point.
      ((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
⊢ x ≡ y
BY
{ (ExRepD THEN (InstLemma `geo-sep-or` [⌜eu⌝;⌜fst(l)⌝;⌜fst(snd(l))⌝;⌜z⌝]⋅ THEN EAuto 1) THEN D -1) }

1
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
      ((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(l) ≠ z
⊢ x ≡ y

2
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
      ((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(snd(l)) ≠ z
⊢ x ≡ y

---

Latex:

---

Latex:

1.  eu  :  EuclideanParPlane@i'
2.  l  :  Line@i
3.  m  :  Line@i
4.  x  :  Point@i
5.  y  :  Point@i
6.  l  \mbackslash{}/  m
7.  x  I  l
8.  x  I  m
9.  y  I  l
10.  y  I  m
11.  \mexists{}z:Point.  (z  I  l  \mwedge{}  z  \#  m)
12.  \mforall{}a,b,c,d,p,q:Point.
            ((\mneg{}Colinear(a;b;c))
            {}\mRightarrow{}  c  \mneq{}  d
            {}\mRightarrow{}  Colinear(a;b;p)
            {}\mRightarrow{}  Colinear(a;b;q)
            {}\mRightarrow{}  Colinear(c;d;p)
            {}\mRightarrow{}  Colinear(c;d;q)
            {}\mRightarrow{}  p  \mequiv{}  q)
\mvdash{}  x  \mequiv{}  y


By

---

Latex:
(ExRepD  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}fst(l)\mkleeneclose{};\mkleeneopen{}fst(snd(l))\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)  THEN  D  -1)

---

Home Index