---

Step * 2 1 of Lemma unique-angles-in-half-plane


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. ∃f:Point. (acb ≅a fzy ∧ (x leftof yz ⇐⇒ f leftof yz) ∧ (x leftof zy ⇐⇒ f leftof zy))
11. f1 : Point
12. f2 : Point
13. acb ≅a f1zy
14. acb ≅a f2zy
15. x leftof yz ⇒ f1 leftof yz
16. x leftof yz ⇐ f1 leftof yz
17. x leftof zy ⇒ f1 leftof zy
18. x leftof zy ⇐ f1 leftof zy
19. x leftof yz ⇒ f2 leftof yz
20. x leftof yz ⇐ f2 leftof yz
21. x leftof zy ⇒ f2 leftof zy
22. x leftof zy ⇐ f2 leftof zy
23. f2zy ≅a f1zy
⊢ Colinear(z;f1;f2)
BY
{ ((Unfold `geo-cong-angle` -1 THEN ExRepD)
   THEN (Assert {z' ≡ c' ∧ ya' ≅ yx'} BY
               ((((InstLemma `geo-inner-three-segment` [⌜e⌝]⋅ THEN Auto)
                  THEN InstHyp [⌜c'⌝;⌜y⌝;⌜z⌝;⌜z'⌝;⌜y⌝;⌜z⌝] (-1)⋅
                  THEN Auto)
                 THEN (InstLemma `geo-construction-unicity` [⌜e⌝;⌜z⌝;⌜y⌝;⌜z'⌝;⌜c'⌝]⋅ THENA Auto)
                 )
                THEN (InstLemma `geo-inner-five-segment` [⌜e⌝;⌜z⌝;⌜y⌝;⌜c'⌝;⌜a'⌝;⌜z⌝;⌜y⌝;⌜z'⌝;⌜x'⌝]⋅ THENA Auto)
                THEN D 0
                THEN Auto))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. f : Point
11. acb ≅a fzy
12. x leftof yz ⇐⇒ f leftof yz
13. x leftof zy ⇐⇒ f leftof zy
14. f1 : Point
15. f2 : Point
16. acb ≅a f1zy
17. acb ≅a f2zy
18. x leftof yz ⇒ f1 leftof yz
19. x leftof yz ⇐ f1 leftof yz
20. x leftof zy ⇒ f1 leftof zy
21. x leftof zy ⇐ f1 leftof zy
22. x leftof yz ⇒ f2 leftof yz
23. x leftof yz ⇐ f2 leftof yz
24. x leftof zy ⇒ f2 leftof zy
25. x leftof zy ⇐ f2 leftof zy
26. f2 # z
27. z # y
28. f1 # z
29. z # y
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. B(zf2a')
35. B(zyc')
36. B(zf1x')
37. B(zyz')
38. za' ≅ zx'
39. zc' ≅ zz'
40. a'c' ≅ x'z'
41. {z' ≡ c' ∧ ya' ≅ yx'}
⊢ Colinear(z;f1;f2)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a  \#  bc
9.  x  \#  yz
10.  \mexists{}f:Point.  (acb  \mcong{}\msuba{}  fzy  \mwedge{}  (x  leftof  yz  \mLeftarrow{}{}\mRightarrow{}  f  leftof  yz)  \mwedge{}  (x  leftof  zy  \mLeftarrow{}{}\mRightarrow{}  f  leftof  zy))
11.  f1  :  Point
12.  f2  :  Point
13.  acb  \mcong{}\msuba{}  f1zy
14.  acb  \mcong{}\msuba{}  f2zy
15.  x  leftof  yz  {}\mRightarrow{}  f1  leftof  yz
16.  x  leftof  yz  \mLeftarrow{}{}  f1  leftof  yz
17.  x  leftof  zy  {}\mRightarrow{}  f1  leftof  zy
18.  x  leftof  zy  \mLeftarrow{}{}  f1  leftof  zy
19.  x  leftof  yz  {}\mRightarrow{}  f2  leftof  yz
20.  x  leftof  yz  \mLeftarrow{}{}  f2  leftof  yz
21.  x  leftof  zy  {}\mRightarrow{}  f2  leftof  zy
22.  x  leftof  zy  \mLeftarrow{}{}  f2  leftof  zy
23.  f2zy  \mcong{}\msuba{}  f1zy
\mvdash{}  Colinear(z;f1;f2)


By

---

Latex:
((Unfold  `geo-cong-angle`  -1  THEN  ExRepD)
  THEN  (Assert  \{z'  \mequiv{}  c'  \mwedge{}  ya'  \mcong{}  yx'\}  BY
                          ((((InstLemma  `geo-inner-three-segment`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)
                                THEN  InstHyp  [\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  (-1)\mcdot{}
                                THEN  Auto)
                              THEN  (InstLemma  `geo-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              )
                            THEN  (InstLemma  `geo-inner-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
                                        THENA  Auto
                                        )
                            THEN  D  0
                            THEN  Auto))
  )

---

Home Index