---

Step * 1 1 1 1 1 of Lemma geo-intersect-lines-iff


1. e : EuclideanPlane
2. p : Line
3. l : Line
4. a : Point
5. b : Point
6. c : Point
7. d : Point
8. v : Point
9. a-v-b
10. c-v-d
11. a I p
12. b I p
13. c I l
14. d I l
15. a leftof cd
16. b leftof dc
17. c leftof ba
18. d leftof ab
19. Colinear(a;fst(p);fst(snd(p)))
20. a # cd
⊢ a # fst(l)fst(snd(l))
BY
{ (GetLinePoints 3 THEN InstLemma `colinear-lsep-general` [⌜e⌝;⌜c⌝;⌜d⌝;⌜x⌝;⌜y⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. p : Line
3. x : Point
4. y : Point
5. l2 : x ≠ y
6. a : Point
7. b : Point
8. c : Point
9. d : Point
10. v : Point
11. a-v-b
12. c-v-d
13. a I p
14. b I p
15. c I <x, y, l2>
16. d I <x, y, l2>
17. a leftof cd
18. b leftof dc
19. c leftof ba
20. d leftof ab
21. Colinear(a;fst(p);fst(snd(p)))
22. a # cd
⊢ Colinear(c;d;x)

2
.....antecedent..... 
1. e : EuclideanPlane
2. p : Line
3. x : Point
4. y : Point
5. l2 : x ≠ y
6. a : Point
7. b : Point
8. c : Point
9. d : Point
10. v : Point
11. a-v-b
12. c-v-d
13. a I p
14. b I p
15. c I <x, y, l2>
16. d I <x, y, l2>
17. a leftof cd
18. b leftof dc
19. c leftof ba
20. d leftof ab
21. Colinear(a;fst(p);fst(snd(p)))
22. a # cd
⊢ Colinear(c;d;y)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Line
3.  l  :  Line
4.  a  :  Point
5.  b  :  Point
6.  c  :  Point
7.  d  :  Point
8.  v  :  Point
9.  a-v-b
10.  c-v-d
11.  a  I  p
12.  b  I  p
13.  c  I  l
14.  d  I  l
15.  a  leftof  cd
16.  b  leftof  dc
17.  c  leftof  ba
18.  d  leftof  ab
19.  Colinear(a;fst(p);fst(snd(p)))
20.  a  \#  cd
\mvdash{}  a  \#  fst(l)fst(snd(l))


By

---

Latex:
(GetLinePoints  3  THEN  InstLemma  `colinear-lsep-general`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index