---

Step * 1 2 1 1 of Lemma common-P_point-intersecting-P_lines2


1. e : EuclideanParPlane
2. p : Point
3. l : Line
4. n : Line
5. P4 : p I n
6. P5 : p # l
7. l2 : Line
8. L3 : p:Point × n:{n:Line| p I n}  × p # l2
9. l1 : Line
10. L2 : p:Point × n:{n:Line| p I n}  × p # l1
11. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
12. ¬((l \/ l1 ∨ n \/ l1) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l1))
13. l2 \/ l1
14. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
15. l1 \/ l
16. l1 \/ n
17. l1 \/ l ⇐ (l1 # l) ∧ (∃x:Point. (x I l1 ∧ x I l))
18. (l1 # l)
19. x : Point
20. x I l1
21. x I l
22. x I l
⊢ x I n
BY
{ (Assert ⌜¬x # n⌝⋅
   THENA ((D 0 THENA Auto) THEN (InstLemma `geo-intersect-lines-iff` [⌜e⌝;⌜l1⌝;⌜n⌝]⋅ THEN EAuto 1) THEN ExRepD)
   ) }

1
1. e : EuclideanParPlane
2. p : Point
3. l : Line
4. n : Line
5. P4 : p I n
6. P5 : p # l
7. l2 : Line
8. L3 : p:Point × n:{n:Line| p I n}  × p # l2
9. l1 : Line
10. L2 : p:Point × n:{n:Line| p I n}  × p # l1
11. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
12. ¬((l \/ l1 ∨ n \/ l1) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l1))
13. l2 \/ l1
14. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
15. l1 \/ l
16. l1 \/ n
17. l1 \/ l ⇐ (l1 # l) ∧ (∃x:Point. (x I l1 ∧ x I l))
18. (l1 # l)
19. x : Point
20. x I l1
21. x I l
22. x I l
23. x # n
24. l1 \/ n ⇐ (l1 # n) ∧ (∃x:Point. (x I l1 ∧ x I n))
25. (l1 # n)
26. x1 : Point
27. x1 I l1
28. x1 I n
⊢ False

2
1. e : EuclideanParPlane
2. p : Point
3. l : Line
4. n : Line
5. P4 : p I n
6. P5 : p # l
7. l2 : Line
8. L3 : p:Point × n:{n:Line| p I n}  × p # l2
9. l1 : Line
10. L2 : p:Point × n:{n:Line| p I n}  × p # l1
11. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
12. ¬((l \/ l1 ∨ n \/ l1) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l1))
13. l2 \/ l1
14. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
15. l1 \/ l
16. l1 \/ n
17. l1 \/ l ⇐ (l1 # l) ∧ (∃x:Point. (x I l1 ∧ x I l))
18. (l1 # l)
19. x : Point
20. x I l1
21. x I l
22. x I l
23. ¬x # n
⊢ x I n

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  p  :  Point
3.  l  :  Line
4.  n  :  Line
5.  P4  :  p  I  n
6.  P5  :  p  \#  l
7.  l2  :  Line
8.  L3  :  p:Point  \mtimes{}  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l2
9.  l1  :  Line
10.  L2  :  p:Point  \mtimes{}  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l1
11.  \mneg{}((l  \mbackslash{}/  l2  \mvee{}  n  \mbackslash{}/  l2)  \mwedge{}  (\mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l2))
12.  \mneg{}((l  \mbackslash{}/  l1  \mvee{}  n  \mbackslash{}/  l1)  \mwedge{}  (\mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l1))
13.  l2  \mbackslash{}/  l1
14.  \mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))
15.  l1  \mbackslash{}/  l
16.  l1  \mbackslash{}/  n
17.  l1  \mbackslash{}/  l  \mLeftarrow{}{}  (l1  \#  l)  \mwedge{}  (\mexists{}x:Point.  (x  I  l1  \mwedge{}  x  I  l))
18.  (l1  \#  l)
19.  x  :  Point
20.  x  I  l1
21.  x  I  l
22.  x  I  l
\mvdash{}  x  I  n


By

---

Latex:
(Assert  \mkleeneopen{}\mneg{}x  \#  n\mkleeneclose{}\mcdot{}
  THENA  ((D  0  THENA  Auto)
                THEN  (InstLemma  `geo-intersect-lines-iff`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
                THEN  ExRepD)
  )

---

Home Index