![]() |
Metamath
Proof Explorer Theorem List (p. 286 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | perpln1 28501 | Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄(βGβπΊ)π΅) β β’ (π β π΄ β ran πΏ) | ||
Theorem | perpln2 28502 | Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄(βGβπΊ)π΅) β β’ (π β π΅ β ran πΏ) | ||
Theorem | isperp 28503* | 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 28504 | 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 28505 | 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 28506* | 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 28507 | One direction of isperp2 28506. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π΅ β ran πΏ) & β’ (π β π β (π΄ β© π΅)) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ (π β π΄(βGβπΊ)π΅) β β’ (π β β¨βπππββ© β (βGβπΊ)) | ||
Theorem | ragperp 28508 | 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 28509* | Alternative version of footex 28512 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 28510 | Lemma for footex 28512. (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 28511 | Lemma for footex 28512. (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 28512* | From a point πΆ outside of a line π΄, there exists a point π₯ on π΄ such that (πΆπΏπ₯) is perpendicular to π΄. This point is unique, see foot 28513. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β πΆ β π) & β’ (π β Β¬ πΆ β π΄) β β’ (π β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) | ||
Theorem | foot 28513* | 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 28514 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β (ππΏπ)(βGβπΊ)π΄) β β’ (π β Β¬ π β π΄) | ||
Theorem | footeq 28515 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β (ππΏπ)(βGβπΊ)π΄) & β’ (π β (ππΏπ)(βGβπΊ)π΄) β β’ (π β π = π) | ||
Theorem | hlperpnel 28516 | 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 28517 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β (π΄πΏπ΅)) & β’ (π β π· β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(πΆπΏπ·)) β β’ (π β β¨βπ΄πΆπ·ββ© β (βGβπΊ)) | ||
Theorem | perpdragALT 28518 | 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 28519 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π·) & β’ (π β π΅ β π·) & β’ (π β πΆ β π) & β’ (π β π·(βGβπΊ)(π΅πΏπΆ)) β β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) | ||
Theorem | colperp 28520 | Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)π·) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) & β’ (π β π΄ β πΆ) β β’ (π β (π΄πΏπΆ)(βGβπΊ)π·) | ||
Theorem | colperpexlem1 28521 | Lemma for colperp 28520. 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 28522 | Lemma for colperpex 28524. 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 28523* | Lemma for colperpex 28524. 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 28524* | 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 28525 | Lemma for opphllem 28526, which is itself used for mideu 28529. (Contributed by Thierry Arnoux, 19-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(ππΏπ΅)) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(π΄πΏπ)) & β’ (π β π β (π΄πΏπ΅)) & β’ (π β π β (ππΌπ)) & β’ (π β π β π) & β’ (π β π β (π΅πΌπ)) & β’ (π β (π΄ β π) = (π΅ β π )) & β’ (π β π β π) & β’ (π β π β (ππΌπ΅)) & β’ (π β π β (π πΌπ)) & β’ (π β π β π) & β’ (π β π β (((πβπ΄)βπ)πΌπ)) & β’ (π β (π β π) = (π β π )) & β’ (π β π β π) & β’ (π β π = ((πβπ)βπ)) β β’ (π β π΅ = π) | ||
Theorem | opphllem 28526* | Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 28527 and later for opphl 28545. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ π = (pInvGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(ππΏπ΅)) & β’ (π β (π΄πΏπ΅)(βGβπΊ)(π΄πΏπ)) & β’ (π β π β (π΄πΏπ΅)) & β’ (π β π β (ππΌπ)) & β’ (π β π β π) & β’ (π β π β (π΅πΌπ)) & β’ (π β (π΄ β π) = (π΅ β π )) β β’ (π β βπ₯ β π (π΅ = ((πβπ₯)βπ΄) β§ π = ((πβπ₯)βπ ))) | ||
Theorem | mideulem 28527* | Lemma for mideu 28529. 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 28528* | 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 28529* | 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 28530* | 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 28531* | Deduce that π΄ and π΅ lie on opposite sides of line πΏ. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π·) & β’ (π β Β¬ π΄ β π·) & β’ (π β Β¬ π΅ β π·) & β’ (π β πΆ β (π΄πΌπ΅)) β β’ (π β π΄ππ΅) | ||
Theorem | oppne1 28532* | 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 28533* | 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 28534* | 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 28535* | 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 28536* | 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 28537* | The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) β β’ (π β Β¬ π΄ππ΄) | ||
Theorem | opphllem1 28538* | Lemma for opphl 28545. (Contributed by Thierry Arnoux, 20-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π΄ππΆ) & β’ (π β π β π·) & β’ (π β π΄ = (πβπΆ)) & β’ (π β π΄ β π ) & β’ (π β π΅ β π ) & β’ (π β π΅ β (π πΌπ΄)) β β’ (π β π΅ππΆ) | ||
Theorem | opphllem2 28539* | Lemma for opphl 28545. Lemma 9.3 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π΄ππΆ) & β’ (π β π β π·) & β’ (π β π΄ = (πβπΆ)) & β’ (π β π΄ β π ) & β’ (π β π΅ β π ) & β’ (π β (π΄ β (π πΌπ΅) β¨ π΅ β (π πΌπ΄))) β β’ (π β π΅ππΆ) | ||
Theorem | opphllem3 28540* | Lemma for opphl 28545: 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 28541* | Lemma for opphl 28545. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β π β π) & β’ (π β π΄ππΆ) & β’ (π β π·(βGβπΊ)(π΄πΏπ )) & β’ (π β π·(βGβπΊ)(πΆπΏπ)) & β’ (π β π β π) & β’ (π β (π β πΆ)(β€GβπΊ)(π β π΄)) & β’ (π β π β π) & β’ (π β (πβπ ) = π) & β’ (π β π β π) & β’ (π β π(πΎβπ )π΄) & β’ (π β π(πΎβπ)πΆ) β β’ (π β πππ) | ||
Theorem | opphllem5 28542* | 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 28543* | 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 28544* | Restating colperpex 28524 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 28545* | 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 28546* | 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 28547* | An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π) & β’ (π β π· β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ(πΎβπ΅)π·) & β’ (π β π΄ β (ππΌπΆ)) β β’ (π β βπ β π (π΄(πΎβπ΅)π β§ π β (ππΌπ·))) | ||
Syntax | chpg 28548 | "Belong to the same open half-plane" relation for points in a geometry. |
class hpG | ||
Definition | df-hpg 28549* | Define the open half plane relation for a geometry πΊ. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 28551 to find the same formulation. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ hpG = (π β V β¦ (π β ran (LineGβπ) β¦ {β¨π, πβ© β£ [(Baseβπ) / π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)))})) | ||
Theorem | ishpg 28550* | 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 28551* | 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 28552* | 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 28553* | 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 28554* | Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ππΆ) β β’ (π β (π΅ππΆ β π΄((hpGβπΊ)βπ·)π΅)) | ||
Theorem | lnoppnhpg 28555* | 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 28556* | 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 28557* | 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 28558* | 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 28559* | 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 28560* | 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 28561* | 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 28562* | 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 28563 | Declare the constant for the midpoint operation. |
class midG | ||
Syntax | clmi 28564 | Declare the constant for the line mirroring function. |
class lInvG | ||
Definition | df-mid 28565* | Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 28569, midbtwn 28570, and midcgr 28571. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
β’ midG = (π β V β¦ (π β (Baseβπ), π β (Baseβπ) β¦ (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ)))) | ||
Definition | df-lmi 28566* | Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 28578. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ lInvG = (π β V β¦ (π β ran (LineGβπ) β¦ (π β (Baseβπ) β¦ (β©π β (Baseβπ)((π(midGβπ)π) β π β§ (π(βGβπ)(π(LineGβπ)π) β¨ π = π)))))) | ||
Theorem | midf 28567 | Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β (midGβπΊ):(π Γ π)βΆπ) | ||
Theorem | midcl 28568 | Closure of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β π) | ||
Theorem | ismidb 28569 | Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (pInvGβπΊ) & β’ (π β π β π) β β’ (π β (π΅ = ((πβπ)βπ΄) β (π΄(midGβπΊ)π΅) = π)) | ||
Theorem | midbtwn 28570 | Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β (π΄πΌπ΅)) | ||
Theorem | midcgr 28571 | Congruence of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄(midGβπΊ)π΅) = πΆ) β β’ (π β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | midid 28572 | Midpoint of a null segment. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΄) = π΄) | ||
Theorem | midcom 28573 | Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) = (π΅(midGβπΊ)π΄)) | ||
Theorem | mirmid 28574 | Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π β π) β β’ (π β ((πβπ΄)(midGβπΊ)(πβπ΅)) = (πβ(π΄(midGβπΊ)π΅))) | ||
Theorem | lmieu 28575* | 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 28576 | Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) β β’ (π β π:πβΆπ) | ||
Theorem | lmicl 28577 | Closure of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β π) | ||
Theorem | islmib 28578 | 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 28579 | 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 28580 | 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 28581* | 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 28582 | 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 28583 | 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 28584 | The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΄ β π·) β β’ (π β (πβπ΄) = π΄) | ||
Theorem | lmimid 28585 | 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 28586 | 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 28587 | Lemma for lmiiso 28588. (Contributed by Thierry Arnoux, 14-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ π = ((π΄(midGβπΊ)(πβπ΄))(midGβπΊ)(π΅(midGβπΊ)(πβπ΅))) β β’ (π β ((πβπ΄) β (πβπ΅)) = (π΄ β π΅)) | ||
Theorem | lmiiso 28588 | 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 28589 | 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 28590 | Lemma for hypcgr 28592, 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 28591 | Lemma for hypcgr 28592, 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 28592 | 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 28593* | 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 28594* | 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 28595* | 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 28596* | Lemma for trgcopyeu 28597. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ π = {β¨π, πβ© β£ ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))} & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β’ (π β π = π) | ||
Theorem | trgcopyeu 28597* | 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 28598 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 28599* | Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 28600 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 28600* | 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 28621 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |