---

Step * 1 1 1 of Lemma eu-colinear-append


1. e : EuclideanPlane
2. L1 : Point List
3. L2 : Point List
4. A : Point
5. B : Point
6. ¬(A = B ∈ Point)
7. (A ∈ L1)
8. (A ∈ L2)
9. (B ∈ L1)
10. (B ∈ L2)
11. (∀A∈L1.(∀B∈L1.(∀C∈L1.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
12. (∀A∈L2.(∀B∈L2.(∀C∈L2.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
13. (∀C∈L1.Colinear(A;B;C))
14. (∀C∈L2.Colinear(A;B;C))
15. ∀C:Point. ((C ∈ L1 @ L2) ⇒ Colinear(A;B;C))
16. A1 : Point
17. (A1 ∈ L1 @ L2)
18. B1 : Point
19. (B1 ∈ L1 @ L2)
20. C : Point
21. (C ∈ L1 @ L2)
22. ¬(A1 = B1 ∈ Point)
23. Colinear(A;B;A1) ∧ Colinear(A;B;B1) ∧ Colinear(A;B;C)
⊢ Colinear(A1;B1;C)
BY
{ (StableCases ⌜A1 = A ∈ Point⌝⋅ THENA Auto) }

1
1. e : EuclideanPlane
2. L1 : Point List
3. L2 : Point List
4. A : Point
5. B : Point
6. ¬(A = B ∈ Point)
7. (A ∈ L1)
8. (A ∈ L2)
9. (B ∈ L1)
10. (B ∈ L2)
11. (∀A∈L1.(∀B∈L1.(∀C∈L1.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
12. (∀A∈L2.(∀B∈L2.(∀C∈L2.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
13. (∀C∈L1.Colinear(A;B;C))
14. (∀C∈L2.Colinear(A;B;C))
15. ∀C:Point. ((C ∈ L1 @ L2) ⇒ Colinear(A;B;C))
16. A1 : Point
17. (A1 ∈ L1 @ L2)
18. B1 : Point
19. (B1 ∈ L1 @ L2)
20. C : Point
21. (C ∈ L1 @ L2)
22. ¬(A1 = B1 ∈ Point)
23. Colinear(A;B;A1) ∧ Colinear(A;B;B1) ∧ Colinear(A;B;C)
24. A1 = A ∈ Point
⊢ Colinear(A1;B1;C)

2
1. e : EuclideanPlane
2. L1 : Point List
3. L2 : Point List
4. A : Point
5. B : Point
6. ¬(A = B ∈ Point)
7. (A ∈ L1)
8. (A ∈ L2)
9. (B ∈ L1)
10. (B ∈ L2)
11. (∀A∈L1.(∀B∈L1.(∀C∈L1.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
12. (∀A∈L2.(∀B∈L2.(∀C∈L2.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
13. (∀C∈L1.Colinear(A;B;C))
14. (∀C∈L2.Colinear(A;B;C))
15. ∀C:Point. ((C ∈ L1 @ L2) ⇒ Colinear(A;B;C))
16. A1 : Point
17. (A1 ∈ L1 @ L2)
18. B1 : Point
19. (B1 ∈ L1 @ L2)
20. C : Point
21. (C ∈ L1 @ L2)
22. ¬(A1 = B1 ∈ Point)
23. Colinear(A;B;A1) ∧ Colinear(A;B;B1) ∧ Colinear(A;B;C)
24. ¬(A1 = A ∈ Point)
⊢ Colinear(A1;B1;C)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  L1  :  Point  List
3.  L2  :  Point  List
4.  A  :  Point
5.  B  :  Point
6.  \mneg{}(A  =  B)
7.  (A  \mmember{}  L1)
8.  (A  \mmember{}  L2)
9.  (B  \mmember{}  L1)
10.  (B  \mmember{}  L2)
11.  (\mforall{}A\mmember{}L1.(\mforall{}B\mmember{}L1.(\mforall{}C\mmember{}L1.(\mneg{}(A  =  B))  {}\mRightarrow{}  Colinear(A;B;C))))
12.  (\mforall{}A\mmember{}L2.(\mforall{}B\mmember{}L2.(\mforall{}C\mmember{}L2.(\mneg{}(A  =  B))  {}\mRightarrow{}  Colinear(A;B;C))))
13.  (\mforall{}C\mmember{}L1.Colinear(A;B;C))
14.  (\mforall{}C\mmember{}L2.Colinear(A;B;C))
15.  \mforall{}C:Point.  ((C  \mmember{}  L1  @  L2)  {}\mRightarrow{}  Colinear(A;B;C))
16.  A1  :  Point
17.  (A1  \mmember{}  L1  @  L2)
18.  B1  :  Point
19.  (B1  \mmember{}  L1  @  L2)
20.  C  :  Point
21.  (C  \mmember{}  L1  @  L2)
22.  \mneg{}(A1  =  B1)
23.  Colinear(A;B;A1)  \mwedge{}  Colinear(A;B;B1)  \mwedge{}  Colinear(A;B;C)
\mvdash{}  Colinear(A1;B1;C)


By

---

Latex:
(StableCases  \mkleeneopen{}A1  =  A\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index