---

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

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  (a # bc
  ⇒ x # yz
  ⇒ ((∃f:Point. (acb ≅a fzy ∧ (x leftof yz ⇐⇒ f leftof yz) ∧ (x leftof zy ⇐⇒ f leftof zy)))
     ∧ (∀f1,f2:Point.
          ((acb ≅a f1zy ∧ acb ≅a f2zy)
          ⇒ (((x leftof yz ⇐⇒ f1 leftof yz) ∧ (x leftof zy ⇐⇒ f1 leftof zy))
             ∧ (x leftof yz ⇐⇒ f2 leftof yz)
             ∧ (x leftof zy ⇐⇒ f2 leftof zy))
          ⇒ Colinear(z;f1;f2)))))
BY
{ 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
⊢ ∃f:Point. (acb ≅a fzy ∧ (x leftof yz ⇐⇒ f leftof yz) ∧ (x leftof zy ⇐⇒ f leftof zy))

2
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
⊢ Colinear(z;f1;f2)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    (a  \#  bc
    {}\mRightarrow{}  x  \#  yz
    {}\mRightarrow{}  ((\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)))
          \mwedge{}  (\mforall{}f1,f2:Point.
                    ((acb  \mcong{}\msuba{}  f1zy  \mwedge{}  acb  \mcong{}\msuba{}  f2zy)
                    {}\mRightarrow{}  (((x  leftof  yz  \mLeftarrow{}{}\mRightarrow{}  f1  leftof  yz)  \mwedge{}  (x  leftof  zy  \mLeftarrow{}{}\mRightarrow{}  f1  leftof  zy))
                          \mwedge{}  (x  leftof  yz  \mLeftarrow{}{}\mRightarrow{}  f2  leftof  yz)
                          \mwedge{}  (x  leftof  zy  \mLeftarrow{}{}\mRightarrow{}  f2  leftof  zy))
                    {}\mRightarrow{}  Colinear(z;f1;f2)))))


By

---

Latex:
Auto

---

Home Index