![]() |
Metamath
Proof Explorer Theorem List (p. 281 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isperp 28001* | Property for 2 lines A, B to be perpendicular. Item (ii) of definition 8.11 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π΅ β ran πΏ) β β’ (π β (π΄(βGβπΊ)π΅ β βπ₯ β (π΄ β© π΅)βπ’ β π΄ βπ£ β π΅ β¨βπ’π₯π£ββ© β (βGβπΊ))) | ||
Theorem | perpcom 28002 | The "perpendicular" relation commutes. Theorem 8.12 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π΅ β ran πΏ) & β’ (π β π΄(βGβπΊ)π΅) β β’ (π β π΅(βGβπΊ)π΄) | ||
Theorem | perpneq 28003 | Two perpendicular lines are different. Theorem 8.14 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π΅ β ran πΏ) & β’ (π β π΄(βGβπΊ)π΅) β β’ (π β π΄ β π΅) | ||
Theorem | isperp2 28004* | Property for 2 lines A, B, intersecting at a point X to be perpendicular. Item (i) of definition 8.13 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π΅ β ran πΏ) & β’ (π β π β (π΄ β© π΅)) β β’ (π β (π΄(βGβπΊ)π΅ β βπ’ β π΄ βπ£ β π΅ β¨βπ’ππ£ββ© β (βGβπΊ))) | ||
Theorem | isperp2d 28005 | One direction of isperp2 28004. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π΅ β ran πΏ) & β’ (π β π β (π΄ β© π΅)) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ (π β π΄(βGβπΊ)π΅) β β’ (π β β¨βπππββ© β (βGβπΊ)) | ||
Theorem | ragperp 28006 | Deduce that two lines are perpendicular from a right angle statement. One direction of theorem 8.13 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 20-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π΅ β ran πΏ) & β’ (π β π β (π΄ β© π΅)) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπππββ© β (βGβπΊ)) β β’ (π β π΄(βGβπΊ)π΅) | ||
Theorem | footexALT 28007* | Alternative version of footex 28010 which minimization requires a notably long time. (Contributed by Thierry Arnoux, 19-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β πΆ β π) & β’ (π β Β¬ πΆ β π΄) β β’ (π β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) | ||
Theorem | footexlem1 28008 | Lemma for footex 28010. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β πΆ β π) & β’ (π β Β¬ πΆ β π΄) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β π) & β’ (π β π΄ = (πΈπΏπΉ)) & β’ (π β πΈ β πΉ) & β’ (π β πΈ β (πΉπΌπ)) & β’ (π β (πΈ β π) = (πΈ β πΆ)) & β’ (π β πΆ = (((pInvGβπΊ)βπ )βπ)) & β’ (π β π β (πΈπΌπ)) & β’ (π β (π β π) = (π β π )) & β’ (π β π β π) & β’ (π β π β (π πΌπ)) & β’ (π β (π β π) = (π β πΈ)) & β’ (π β π β ((((pInvGβπΊ)βπ)βπ)πΌπ·)) & β’ (π β (π β π·) = (π β πΆ)) & β’ (π β π· = (((pInvGβπΊ)βπ)βπΆ)) β β’ (π β π β π΄) | ||
Theorem | footexlem2 28009 | Lemma for footex 28010. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β πΆ β π) & β’ (π β Β¬ πΆ β π΄) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β π) & β’ (π β π΄ = (πΈπΏπΉ)) & β’ (π β πΈ β πΉ) & β’ (π β πΈ β (πΉπΌπ)) & β’ (π β (πΈ β π) = (πΈ β πΆ)) & β’ (π β πΆ = (((pInvGβπΊ)βπ )βπ)) & β’ (π β π β (πΈπΌπ)) & β’ (π β (π β π) = (π β π )) & β’ (π β π β π) & β’ (π β π β (π πΌπ)) & β’ (π β (π β π) = (π β πΈ)) & β’ (π β π β ((((pInvGβπΊ)βπ)βπ)πΌπ·)) & β’ (π β (π β π·) = (π β πΆ)) & β’ (π β π· = (((pInvGβπΊ)βπ)βπΆ)) β β’ (π β (πΆπΏπ)(βGβπΊ)π΄) | ||
Theorem | footex 28010* | From a point πΆ outside of a line π΄, there exists a point π₯ on π΄ such that (πΆπΏπ₯) is perpendicular to π΄. This point is unique, see foot 28011. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β πΆ β π) & β’ (π β Β¬ πΆ β π΄) β β’ (π β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) | ||
Theorem | foot 28011* | From a point πΆ outside of a line π΄, there exists a unique point π₯ on π΄ such that (πΆπΏπ₯) is perpendicular to π΄. That point is called the foot from πΆ on π΄. Theorem 8.18 of [Schwabhauser] p. 60. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β πΆ β π) & β’ (π β Β¬ πΆ β π΄) β β’ (π β β!π₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) | ||
Theorem | footne 28012 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β (ππΏπ)(βGβπΊ)π΄) β β’ (π β Β¬ π β π΄) | ||
Theorem | footeq 28013 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β (ππΏπ)(βGβπΊ)π΄) & β’ (π β (ππΏπ)(βGβπΊ)π΄) β β’ (π β π = π) | ||
Theorem | hlperpnel 28014 | A point on a half-line which is perpendicular to a line cannot be on that line. (Contributed by Thierry Arnoux, 1-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄(βGβπΊ)(ππΏπ)) & β’ (π β π(πΎβπ)π) β β’ (π β Β¬ π β π΄) | ||
Theorem | perprag 28015 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β (π΄πΏπ΅)) & β’ (π β π· β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(πΆπΏπ·)) β β’ (π β β¨βπ΄πΆπ·ββ© β (βGβπΊ)) | ||
Theorem | perpdragALT 28016 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π·) & β’ (π β π΅ β π·) & β’ (π β πΆ β π) & β’ (π β π·(βGβπΊ)(π΅πΏπΆ)) β β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) | ||
Theorem | perpdrag 28017 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π·) & β’ (π β π΅ β π·) & β’ (π β πΆ β π) & β’ (π β π·(βGβπΊ)(π΅πΏπΆ)) β β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) | ||
Theorem | colperp 28018 | Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)π·) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) & β’ (π β π΄ β πΆ) β β’ (π β (π΄πΏπΆ)(βGβπΊ)π·) | ||
Theorem | colperpexlem1 28019 | Lemma for colperp 28018. First part of lemma 8.20 of [Schwabhauser] p. 62. (Contributed by Thierry Arnoux, 27-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ π = (πβπ΄) & β’ π = (πβπ΅) & β’ πΎ = (πβπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) & β’ (π β (πΎβ(πβπΆ)) = (πβπΆ)) β β’ (π β β¨βπ΅π΄πββ© β (βGβπΊ)) | ||
Theorem | colperpexlem2 28020 | Lemma for colperpex 28022. Second part of lemma 8.20 of [Schwabhauser] p. 62. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ π = (πβπ΄) & β’ π = (πβπ΅) & β’ πΎ = (πβπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) & β’ (π β (πΎβ(πβπΆ)) = (πβπΆ)) & β’ (π β π΅ β πΆ) β β’ (π β π΄ β π) | ||
Theorem | colperpexlem3 28021* | Lemma for colperpex 28022. Case 1 of theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ β π΅) & β’ (π β Β¬ πΆ β (π΄πΏπ΅)) β β’ (π β βπ β π ((π΄πΏπ)(βGβπΊ)(π΄πΏπ΅) β§ βπ‘ β π ((π‘ β (π΄πΏπ΅) β¨ π΄ = π΅) β§ π‘ β (πΆπΌπ)))) | ||
Theorem | colperpex 28022* | In dimension 2 and above, on a line (π΄πΏπ΅) there is always a perpendicular π from π΄ on a given plane (here given by πΆ, in case πΆ does not lie on the line). Theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ β π΅) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β βπ β π ((π΄πΏπ)(βGβπΊ)(π΄πΏπ΅) β§ βπ‘ β π ((π‘ β (π΄πΏπ΅) β¨ π΄ = π΅) β§ π‘ β (πΆπΌπ)))) | ||
Theorem | mideulem2 28023 | Lemma for opphllem 28024, which is itself used for mideu 28027. (Contributed by Thierry Arnoux, 19-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(ππΏπ΅)) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(π΄πΏπ)) & β’ (π β π β (π΄πΏπ΅)) & β’ (π β π β (ππΌπ)) & β’ (π β π β π) & β’ (π β π β (π΅πΌπ)) & β’ (π β (π΄ β π) = (π΅ β π )) & β’ (π β π β π) & β’ (π β π β (ππΌπ΅)) & β’ (π β π β (π πΌπ)) & β’ (π β π β π) & β’ (π β π β (((πβπ΄)βπ)πΌπ)) & β’ (π β (π β π) = (π β π )) & β’ (π β π β π) & β’ (π β π = ((πβπ)βπ)) β β’ (π β π΅ = π) | ||
Theorem | opphllem 28024* | Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 28025 and later for opphl 28043. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(ππΏπ΅)) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(π΄πΏπ)) & β’ (π β π β (π΄πΏπ΅)) & β’ (π β π β (ππΌπ)) & β’ (π β π β π) & β’ (π β π β (π΅πΌπ)) & β’ (π β (π΄ β π) = (π΅ β π )) β β’ (π β βπ₯ β π (π΅ = ((πβπ₯)βπ΄) β§ π = ((πβπ₯)βπ ))) | ||
Theorem | mideulem 28025* | Lemma for mideu 28027. We can assume mideulem.9 "without loss of generality". (Contributed by Thierry Arnoux, 25-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(ππΏπ΅)) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(π΄πΏπ)) & β’ (π β π β (π΄πΏπ΅)) & β’ (π β π β (ππΌπ)) & β’ (π β (π΄ β π)(β€GβπΊ)(π΅ β π)) β β’ (π β βπ₯ β π π΅ = ((πβπ₯)βπ΄)) | ||
Theorem | midex 28026* | Existence of the midpoint, part Theorem 8.22 of [Schwabhauser] p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β βπ₯ β π π΅ = ((πβπ₯)βπ΄)) | ||
Theorem | mideu 28027* | Existence and uniqueness of the midpoint, Theorem 8.22 of [Schwabhauser] p. 64. (Contributed by Thierry Arnoux, 25-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β β!π₯ β π π΅ = ((πβπ₯)βπ΄)) | ||
Theorem | islnopp 28028* | The property for two points π΄ and π΅ to lie on the opposite sides of a set π· Definition 9.1 of [Schwabhauser] p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ππ΅ β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) | ||
Theorem | islnoppd 28029* | Deduce that π΄ and π΅ lie on opposite sides of line πΏ. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π·) & β’ (π β Β¬ π΄ β π·) & β’ (π β Β¬ π΅ β π·) & β’ (π β πΆ β (π΄πΌπ΅)) β β’ (π β π΄ππ΅) | ||
Theorem | oppne1 28030* | Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ππ΅) β β’ (π β Β¬ π΄ β π·) | ||
Theorem | oppne2 28031* | Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ππ΅) β β’ (π β Β¬ π΅ β π·) | ||
Theorem | oppne3 28032* | Points lying on opposite sides of a line cannot be equal. (Contributed by Thierry Arnoux, 3-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ππ΅) β β’ (π β π΄ β π΅) | ||
Theorem | oppcom 28033* | Commutativity rule for "opposite" Theorem 9.2 of [Schwabhauser] p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ππ΅) β β’ (π β π΅ππ΄) | ||
Theorem | opptgdim2 28034* | If two points opposite to a line exist, dimension must be 2 or more. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ππ΅) β β’ (π β πΊDimTarskiGβ₯2) | ||
Theorem | oppnid 28035* | The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) β β’ (π β Β¬ π΄ππ΄) | ||
Theorem | opphllem1 28036* | Lemma for opphl 28043. (Contributed by Thierry Arnoux, 20-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π΄ππΆ) & β’ (π β π β π·) & β’ (π β π΄ = (πβπΆ)) & β’ (π β π΄ β π ) & β’ (π β π΅ β π ) & β’ (π β π΅ β (π πΌπ΄)) β β’ (π β π΅ππΆ) | ||
Theorem | opphllem2 28037* | Lemma for opphl 28043. Lemma 9.3 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π΄ππΆ) & β’ (π β π β π·) & β’ (π β π΄ = (πβπΆ)) & β’ (π β π΄ β π ) & β’ (π β π΅ β π ) & β’ (π β (π΄ β (π πΌπ΅) β¨ π΅ β (π πΌπ΄))) β β’ (π β π΅ππΆ) | ||
Theorem | opphllem3 28038* | Lemma for opphl 28043: We assume opphllem3.l "without loss of generality". (Contributed by Thierry Arnoux, 21-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β π β π) & β’ (π β π΄ππΆ) & β’ (π β π·(βGβπΊ)(π΄πΏπ )) & β’ (π β π·(βGβπΊ)(πΆπΏπ)) & β’ (π β π β π) & β’ (π β (π β πΆ)(β€GβπΊ)(π β π΄)) & β’ (π β π β π) & β’ (π β (πβπ ) = π) β β’ (π β (π(πΎβπ )π΄ β (πβπ)(πΎβπ)πΆ)) | ||
Theorem | opphllem4 28039* | Lemma for opphl 28043. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β π β π) & β’ (π β π΄ππΆ) & β’ (π β π·(βGβπΊ)(π΄πΏπ )) & β’ (π β π·(βGβπΊ)(πΆπΏπ)) & β’ (π β π β π) & β’ (π β (π β πΆ)(β€GβπΊ)(π β π΄)) & β’ (π β π β π) & β’ (π β (πβπ ) = π) & β’ (π β π β π) & β’ (π β π(πΎβπ )π΄) & β’ (π β π(πΎβπ)πΆ) β β’ (π β πππ) | ||
Theorem | opphllem5 28040* | Second part of Lemma 9.4 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β π β π) & β’ (π β π΄ππΆ) & β’ (π β π·(βGβπΊ)(π΄πΏπ )) & β’ (π β π·(βGβπΊ)(πΆπΏπ)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π(πΎβπ )π΄) & β’ (π β π(πΎβπ)πΆ) β β’ (π β πππ) | ||
Theorem | opphllem6 28041* | First part of Lemma 9.4 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β π β π) & β’ (π β π΄ππΆ) & β’ (π β π·(βGβπΊ)(π΄πΏπ )) & β’ (π β π·(βGβπΊ)(πΆπΏπ)) & β’ (π β π β π) & β’ (π β (πβπ ) = π) β β’ (π β (π(πΎβπ )π΄ β (πβπ)(πΎβπ)πΆ)) | ||
Theorem | oppperpex 28042* | Restating colperpex 28022 using the "opposite side of a line" relation. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π·) & β’ (π β πΆ β π) & β’ (π β Β¬ πΆ β π·) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β βπ β π ((π΄πΏπ)(βGβπΊ)π· β§ πΆππ)) | ||
Theorem | opphl 28043* | If two points π΄ and πΆ lie on opposite sides of a line π·, then any point of the half line (π π΄) also lies opposite to πΆ. Theorem 9.5 of [Schwabhauser] p. 69. (Contributed by Thierry Arnoux, 3-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ππΆ) & β’ (π β π β π·) & β’ (π β π΄(πΎβπ )π΅) β β’ (π β π΅ππΆ) | ||
Theorem | outpasch 28044* | Axiom of Pasch, outer form. This was proven by Gupta from other axioms and is therefore presented as Theorem 9.6 in [Schwabhauser] p. 70. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΆ β (π΄πΌπ )) & β’ (π β π β (π΅πΌπΆ)) β β’ (π β βπ₯ β π (π₯ β (π΄πΌπ΅) β§ π β (π πΌπ₯))) | ||
Theorem | hlpasch 28045* | An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π) & β’ (π β π· β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ(πΎβπ΅)π·) & β’ (π β π΄ β (ππΌπΆ)) β β’ (π β βπ β π (π΄(πΎβπ΅)π β§ π β (ππΌπ·))) | ||
Syntax | chpg 28046 | "Belong to the same open half-plane" relation for points in a geometry. |
class hpG | ||
Definition | df-hpg 28047* | Define the open half plane relation for a geometry πΊ. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 28049 to find the same formulation. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ hpG = (π β V β¦ (π β ran (LineGβπ) β¦ {β¨π, πβ© β£ [(Baseβπ) / π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)))})) | ||
Theorem | ishpg 28048* | Value of the half-plane relation for a given line π·. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) β β’ (π β ((hpGβπΊ)βπ·) = {β¨π, πβ© β£ βπ β π (πππ β§ πππ)}) | ||
Theorem | hpgbr 28049* | Half-planes : property for points π΄ and π΅ to belong to the same open half plane delimited by line π·. Definition 9.7 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄((hpGβπΊ)βπ·)π΅ β βπ β π (π΄ππ β§ π΅ππ))) | ||
Theorem | hpgne1 28050* | Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄((hpGβπΊ)βπ·)π΅) β β’ (π β Β¬ π΄ β π·) | ||
Theorem | hpgne2 28051* | Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄((hpGβπΊ)βπ·)π΅) β β’ (π β Β¬ π΅ β π·) | ||
Theorem | lnopp2hpgb 28052* | Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ππΆ) β β’ (π β (π΅ππΆ β π΄((hpGβπΊ)βπ·)π΅)) | ||
Theorem | lnoppnhpg 28053* | If two points lie on the opposite side of a line π·, they are not on the same half-plane. Theorem 9.9 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ππ΅) β β’ (π β Β¬ π΄((hpGβπΊ)βπ·)π΅) | ||
Theorem | hpgerlem 28054* | Lemma for the proof that the half-plane relation is an equivalence relation. Lemma 9.10 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β Β¬ π΄ β π·) β β’ (π β βπ β π π΄ππ) | ||
Theorem | hpgid 28055* | The half-plane relation is reflexive. Theorem 9.11 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β Β¬ π΄ β π·) β β’ (π β π΄((hpGβπΊ)βπ·)π΄) | ||
Theorem | hpgcom 28056* | The half-plane relation commutes. Theorem 9.12 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΅ β π) & β’ (π β π΄((hpGβπΊ)βπ·)π΅) β β’ (π β π΅((hpGβπΊ)βπ·)π΄) | ||
Theorem | hpgtr 28057* | The half-plane relation is transitive. Theorem 9.13 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΅ β π) & β’ (π β π΄((hpGβπΊ)βπ·)π΅) & β’ (π β πΆ β π) & β’ (π β π΅((hpGβπΊ)βπ·)πΆ) β β’ (π β π΄((hpGβπΊ)βπ·)πΆ) | ||
Theorem | colopp 28058* | Opposite sides of a line for colinear points. Theorem 9.18 of [Schwabhauser] p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΅ β π) & β’ (π β πΆ β π·) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β (π΄ππ΅ β (πΆ β (π΄πΌπ΅) β§ Β¬ π΄ β π· β§ Β¬ π΅ β π·))) | ||
Theorem | colhp 28059* | Half-plane relation for colinear points. Theorem 9.19 of [Schwabhauser] p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΅ β π) & β’ (π β πΆ β π·) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) & β’ πΎ = (hlGβπΊ) β β’ (π β (π΄((hpGβπΊ)βπ·)π΅ β (π΄(πΎβπΆ)π΅ β§ Β¬ π΄ β π·))) | ||
Theorem | hphl 28060* | If two points are on the same half-line with endpoint on a line, they are on the same half-plane defined by this line. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π·) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β π·) & β’ (π β π΅(πΎβπ΄)πΆ) β β’ (π β π΅((hpGβπΊ)βπ·)πΆ) | ||
Syntax | cmid 28061 | Declare the constant for the midpoint operation. |
class midG | ||
Syntax | clmi 28062 | Declare the constant for the line mirroring function. |
class lInvG | ||
Definition | df-mid 28063* | Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 28067, midbtwn 28068, and midcgr 28069. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
β’ midG = (π β V β¦ (π β (Baseβπ), π β (Baseβπ) β¦ (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ)))) | ||
Definition | df-lmi 28064* | Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 28076. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ lInvG = (π β V β¦ (π β ran (LineGβπ) β¦ (π β (Baseβπ) β¦ (β©π β (Baseβπ)((π(midGβπ)π) β π β§ (π(βGβπ)(π(LineGβπ)π) β¨ π = π)))))) | ||
Theorem | midf 28065 | Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β (midGβπΊ):(π Γ π)βΆπ) | ||
Theorem | midcl 28066 | Closure of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β π) | ||
Theorem | ismidb 28067 | Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (pInvGβπΊ) & β’ (π β π β π) β β’ (π β (π΅ = ((πβπ)βπ΄) β (π΄(midGβπΊ)π΅) = π)) | ||
Theorem | midbtwn 28068 | Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β (π΄πΌπ΅)) | ||
Theorem | midcgr 28069 | Congruence of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄(midGβπΊ)π΅) = πΆ) β β’ (π β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | midid 28070 | Midpoint of a null segment. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΄) = π΄) | ||
Theorem | midcom 28071 | Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) = (π΅(midGβπΊ)π΄)) | ||
Theorem | mirmid 28072 | Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π β π) β β’ (π β ((πβπ΄)(midGβπΊ)(πβπ΅)) = (πβ(π΄(midGβπΊ)π΅))) | ||
Theorem | lmieu 28073* | Uniqueness of the line mirror point. Theorem 10.2 of [Schwabhauser] p. 88. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β β!π β π ((π΄(midGβπΊ)π) β π· β§ (π·(βGβπΊ)(π΄πΏπ) β¨ π΄ = π))) | ||
Theorem | lmif 28074 | Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) β β’ (π β π:πβΆπ) | ||
Theorem | lmicl 28075 | Closure of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β π) | ||
Theorem | islmib 28076 | Property of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΅ = (πβπ΄) β ((π΄(midGβπΊ)π΅) β π· β§ (π·(βGβπΊ)(π΄πΏπ΅) β¨ π΄ = π΅)))) | ||
Theorem | lmicom 28077 | The line mirroring function is an involution. Theorem 10.4 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (πβπ΄) = π΅) β β’ (π β (πβπ΅) = π΄) | ||
Theorem | lmilmi 28078 | Line mirroring is an involution. Theorem 10.5 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β (πβ(πβπ΄)) = π΄) | ||
Theorem | lmireu 28079* | Any point has a unique antecedent through line mirroring. Theorem 10.6 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β β!π β π (πβπ) = π΄) | ||
Theorem | lmieq 28080 | Equality deduction for line mirroring. Theorem 10.7 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (πβπ΄) = (πβπ΅)) β β’ (π β π΄ = π΅) | ||
Theorem | lmiinv 28081 | The invariants of the line mirroring lie on the mirror line. Theorem 10.8 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β ((πβπ΄) = π΄ β π΄ β π·)) | ||
Theorem | lmicinv 28082 | The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΄ β π·) β β’ (π β (πβπ΄) = π΄) | ||
Theorem | lmimid 28083 | If we have a right angle, then the mirror point is the point inversion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ π = ((pInvGβπΊ)βπ΅) & β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) & β’ (π β π΄ β π·) & β’ (π β π΅ β π·) & β’ (π β πΆ β π) & β’ (π β π΄ β π΅) β β’ (π β (πβπΆ) = (πβπΆ)) | ||
Theorem | lmif1o 28084 | The line mirroring function π is a bijection. Theorem 10.9 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) β β’ (π β π:πβ1-1-ontoβπ) | ||
Theorem | lmiisolem 28085 | Lemma for lmiiso 28086. (Contributed by Thierry Arnoux, 14-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ π = ((π΄(midGβπΊ)(πβπ΄))(midGβπΊ)(π΅(midGβπΊ)(πβπ΅))) β β’ (π β ((πβπ΄) β (πβπ΅)) = (π΄ β π΅)) | ||
Theorem | lmiiso 28086 | The line mirroring function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 10.10 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β ((πβπ΄) β (πβπ΅)) = (π΄ β π΅)) | ||
Theorem | lmimot 28087 | Line mirroring is a motion of the geometric space. Theorem 10.11 of [Schwabhauser] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) β β’ (π β π β (πΊIsmtπΊ)) | ||
Theorem | hypcgrlem1 28088 | Lemma for hypcgr 28090, case where triangles share a cathetus. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) & β’ (π β β¨βπ·πΈπΉββ© β (βGβπΊ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β π΅ = πΈ) & β’ π = ((lInvGβπΊ)β((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)) & β’ (π β πΆ = πΉ) β β’ (π β (π΄ β πΆ) = (π· β πΉ)) | ||
Theorem | hypcgrlem2 28089 | Lemma for hypcgr 28090, case where triangles share one vertex π΅. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) & β’ (π β β¨βπ·πΈπΉββ© β (βGβπΊ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β π΅ = πΈ) & β’ π = ((lInvGβπΊ)β((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)) β β’ (π β (π΄ β πΆ) = (π· β πΉ)) | ||
Theorem | hypcgr 28090 | If the catheti of two right-angled triangles are congruent, so is their hypothenuse. Theorem 10.12 of [Schwabhauser] p. 91. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) & β’ (π β β¨βπ·πΈπΉββ© β (βGβπΊ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) β β’ (π β (π΄ β πΆ) = (π· β πΉ)) | ||
Theorem | lmiopp 28091* | Line mirroring produces points on the opposite side of the mirroring line. Theorem 10.14 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π· β ran πΏ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ π = ((lInvGβπΊ)βπ·) & β’ (π β π΄ β π) & β’ (π β Β¬ π΄ β π·) β β’ (π β π΄π(πβπ΄)) | ||
Theorem | lnperpex 28092* | Existence of a perpendicular to a line πΏ at a given point π΄. Theorem 10.15 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π· β ran πΏ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΄ β π·) & β’ (π β π β π) & β’ (π β Β¬ π β π·) β β’ (π β βπ β π (π·(βGβπΊ)(ππΏπ΄) β§ π((hpGβπΊ)βπ·)π)) | ||
Theorem | trgcopy 28093* | Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) β β’ (π β βπ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) | ||
Theorem | trgcopyeulem 28094* | Lemma for trgcopyeu 28095. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ π = {β¨π, πβ© β£ ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))} & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β’ (π β π = π) | ||
Theorem | trgcopyeu 28095* | Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: uniqueness part. Second part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) β β’ (π β β!π β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) | ||
Syntax | ccgra 28096 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 28097* | Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 28098 for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020.) |
β’ cgrA = (π β V β¦ {β¨π, πβ© β£ [(Baseβπ) / π][(hlGβπ) / π]((π β (π βm (0..^3)) β§ π β (π βm (0..^3))) β§ βπ₯ β π βπ¦ β π (π(cgrGβπ)β¨βπ₯(πβ1)π¦ββ© β§ π₯(πβ(πβ1))(πβ0) β§ π¦(πβ(πβ1))(πβ2)))}) | ||
Theorem | iscgra 28098* | Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of [Schwabhauser] p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 28119 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ))) | ||
Theorem | iscgra1 28099* | A special version of iscgra 28098 where one distance is known to be equal. In this case, angle congruence can be written with only one quantifier. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ β = (distβπΊ) & β’ (π β π΄ β π΅) & β’ (π β (π΄ β π΅) = (π· β πΈ)) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπ₯ββ© β§ π₯(πΎβπΈ)πΉ))) | ||
Theorem | iscgrad 28100 | Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βππΈπββ©) & β’ (π β π(πΎβπΈ)π·) & β’ (π β π(πΎβπΈ)πΉ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |