Home | Metamath
Proof Explorer Theorem List (p. 276 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hpgne1 27501* | 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 27502* | 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 27503* | Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ππΆ) β β’ (π β (π΅ππΆ β π΄((hpGβπΊ)βπ·)π΅)) | ||
Theorem | lnoppnhpg 27504* | 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 27505* | 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 27506* | 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 27507* | 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 27508* | 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 27509* | 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 27510* | 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 27511* | 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 27512 | Declare the constant for the midpoint operation. |
class midG | ||
Syntax | clmi 27513 | Declare the constant for the line mirroring function. |
class lInvG | ||
Definition | df-mid 27514* | Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 27518, midbtwn 27519, and midcgr 27520. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
β’ midG = (π β V β¦ (π β (Baseβπ), π β (Baseβπ) β¦ (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ)))) | ||
Definition | df-lmi 27515* | Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 27527. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ lInvG = (π β V β¦ (π β ran (LineGβπ) β¦ (π β (Baseβπ) β¦ (β©π β (Baseβπ)((π(midGβπ)π) β π β§ (π(βGβπ)(π(LineGβπ)π) β¨ π = π)))))) | ||
Theorem | midf 27516 | Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β (midGβπΊ):(π Γ π)βΆπ) | ||
Theorem | midcl 27517 | Closure of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β π) | ||
Theorem | ismidb 27518 | Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (pInvGβπΊ) & β’ (π β π β π) β β’ (π β (π΅ = ((πβπ)βπ΄) β (π΄(midGβπΊ)π΅) = π)) | ||
Theorem | midbtwn 27519 | Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β (π΄πΌπ΅)) | ||
Theorem | midcgr 27520 | Congruence of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄(midGβπΊ)π΅) = πΆ) β β’ (π β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | midid 27521 | Midpoint of a null segment. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΄) = π΄) | ||
Theorem | midcom 27522 | Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) = (π΅(midGβπΊ)π΄)) | ||
Theorem | mirmid 27523 | Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π β π) β β’ (π β ((πβπ΄)(midGβπΊ)(πβπ΅)) = (πβ(π΄(midGβπΊ)π΅))) | ||
Theorem | lmieu 27524* | 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 27525 | Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) β β’ (π β π:πβΆπ) | ||
Theorem | lmicl 27526 | Closure of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β π) | ||
Theorem | islmib 27527 | 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 27528 | 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 27529 | 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 27530* | 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 27531 | 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 27532 | 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 27533 | The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΄ β π·) β β’ (π β (πβπ΄) = π΄) | ||
Theorem | lmimid 27534 | 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 27535 | 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 27536 | Lemma for lmiiso 27537. (Contributed by Thierry Arnoux, 14-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ π = ((π΄(midGβπΊ)(πβπ΄))(midGβπΊ)(π΅(midGβπΊ)(πβπ΅))) β β’ (π β ((πβπ΄) β (πβπ΅)) = (π΄ β π΅)) | ||
Theorem | lmiiso 27537 | 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 27538 | 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 27539 | Lemma for hypcgr 27541, 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 27540 | Lemma for hypcgr 27541, 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 27541 | 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 27542* | 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 27543* | 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 27544* | 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 27545* | Lemma for trgcopyeu 27546. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ π = {β¨π, πβ© β£ ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))} & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β’ (π β π = π) | ||
Theorem | trgcopyeu 27546* | 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 27547 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 27548* | Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 27549 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 27549* | 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 27570 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ))) | ||
Theorem | iscgra1 27550* | A special version of iscgra 27549 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 27551 | Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βππΈπββ©) & β’ (π β π(πΎβπΈ)π·) & β’ (π β π(πΎβπΈ)πΉ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgrane1 27552 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | cgrane2 27553 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΅ β πΆ) | ||
Theorem | cgrane3 27554 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β π·) | ||
Theorem | cgrane4 27555 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β πΉ) | ||
Theorem | cgrahl1 27556 | Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β π β π) & β’ (π β π(πΎβπΈ)π·) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βππΈπΉββ©) | ||
Theorem | cgrahl2 27557 | Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β π β π) & β’ (π β π(πΎβπΈ)πΉ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) | ||
Theorem | cgracgr 27558 | First direction of proposition 11.4 of [Schwabhauser] p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β π β π) & β’ β = (distβπΊ) & β’ (π β π β π) & β’ (π β π(πΎβπ΅)π΄) & β’ (π β π(πΎβπ΅)πΆ) & β’ (π β (π΅ β π) = (πΈ β π·)) & β’ (π β (π΅ β π) = (πΈ β πΉ)) β β’ (π β (π β π) = (π· β πΉ)) | ||
Theorem | cgraid 27559 | Angle congruence is reflexive. Theorem 11.6 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | cgraswap 27560 | Swap rays in a congruence relation. Theorem 11.9 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπΆπ΅π΄ββ©) | ||
Theorem | cgrcgra 27561 | Triangle congruence implies angle congruence. This is a portion of CPCTC, focusing on a specific angle. (Contributed by Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgracom 27562 | Angle congruence commutes. Theorem 11.7 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | cgratr 27563 | Angle congruence is transitive. Theorem 11.8 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β π» β π) & β’ (π β π β π) & β’ (π β π½ β π) & β’ (π β β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ»ππ½ββ©) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ»ππ½ββ©) | ||
Theorem | flatcgra 27564 | Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΉ)) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π· β πΈ) & β’ (π β πΉ β πΈ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgraswaplr 27565 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β β¨βπΆπ΅π΄ββ©(cgrAβπΊ)β¨βπΉπΈπ·ββ©) | ||
Theorem | cgrabtwn 27566 | Angle congruence preserves flat angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β πΈ β (π·πΌπΉ)) | ||
Theorem | cgrahl 27567 | Angle congruence preserves null angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΎ = (hlGβπΊ) & β’ (π β π΄(πΎβπ΅)πΆ) β β’ (π β π·(πΎβπΈ)πΉ) | ||
Theorem | cgracol 27568 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | cgrancol 27569 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β Β¬ (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | dfcgra2 27570* | This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 27548 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β ((π΄ β π΅ β§ πΆ β π΅) β§ (π· β πΈ β§ πΉ β πΈ) β§ βπ β π βπ β π βπ β π βπ β π (((π΄ β (π΅πΌπ) β§ (π΄ β π) = (πΈ β π·)) β§ (πΆ β (π΅πΌπ) β§ (πΆ β π) = (πΈ β πΉ))) β§ ((π· β (πΈπΌπ) β§ (π· β π) = (π΅ β π΄)) β§ (πΉ β (πΈπΌπ) β§ (πΉ β π) = (π΅ β πΆ))) β§ (π β π) = (π β π))))) | ||
Theorem | sacgr 27571 | Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020.) (Proof shortened by Igor Ieskov, 16-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β π΅ β (π΄πΌπ)) & β’ (π β πΈ β (π·πΌπ)) & β’ (π β π΅ β π) & β’ (π β πΈ β π) β β’ (π β β¨βππ΅πΆββ©(cgrAβπΊ)β¨βππΈπΉββ©) | ||
Theorem | oacgr 27572 | Vertical angle theorem. Vertical, or opposite angles are the facing pair of angles formed when two lines intersect. Eudemus of Rhodes attributed the proof to Thales of Miletus. The proposition showed that since both of a pair of vertical angles are supplementary to both of the adjacent angles, the vertical angles are equal in measure. We follow the same path. Theorem 11.14 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 27-Sep-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπ·)) & β’ (π β π΅ β (πΆπΌπΉ)) & β’ (π β π΅ β π΄) & β’ (π β π΅ β πΆ) & β’ (π β π΅ β π·) & β’ (π β π΅ β πΉ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·π΅πΉββ©) | ||
Theorem | acopy 27573* | Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) β β’ (π β βπ β π (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) | ||
Theorem | acopyeu 27574 | Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points π and π both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΎ = (hlGβπΊ) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β’ (π β π(πΎβπΈ)π) | ||
Syntax | cinag 27575 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 27576 | Extend class relation with the "angle less than" relation. |
class β€β | ||
Definition | df-inag 27577* | Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
β’ inA = (π β V β¦ {β¨π, π‘β© β£ ((π β (Baseβπ) β§ π‘ β ((Baseβπ) βm (0..^3))) β§ (((π‘β0) β (π‘β1) β§ (π‘β2) β (π‘β1) β§ π β (π‘β1)) β§ βπ₯ β (Baseβπ)(π₯ β ((π‘β0)(Itvβπ)(π‘β2)) β§ (π₯ = (π‘β1) β¨ π₯((hlGβπ)β(π‘β1))π))))}) | ||
Theorem | isinag 27578* | Property for point π to lie in the angle β¨βπ΄π΅πΆββ©. Definition 11.23 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β π) β β’ (π β (π(inAβπΊ)β¨βπ΄π΅πΆββ© β ((π΄ β π΅ β§ πΆ β π΅ β§ π β π΅) β§ βπ₯ β π (π₯ β (π΄πΌπΆ) β§ (π₯ = π΅ β¨ π₯(πΎβπ΅)π))))) | ||
Theorem | isinagd 27579 | Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π β (π΄πΌπΆ)) & β’ (π β (π = π΅ β¨ π(πΎβπ΅)π)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagflat 27580 | Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagswap 27581 | Swap the order of the half lines delimiting the angle. Theorem 11.24 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π(inAβπΊ)β¨βπΆπ΅π΄ββ©) | ||
Theorem | inagne1 27582 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π΄ β π΅) | ||
Theorem | inagne2 27583 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β πΆ β π΅) | ||
Theorem | inagne3 27584 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π β π΅) | ||
Theorem | inaghl 27585 | The "point lie in angle" relation is independent of the points chosen on the half lines starting from π΅. Theorem 11.25 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 27-Sep-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) & β’ (π β π· β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π·(πΎβπ΅)π΄) & β’ (π β πΉ(πΎβπ΅)πΆ) & β’ (π β π(πΎβπ΅)π) β β’ (π β π(inAβπΊ)β¨βπ·π΅πΉββ©) | ||
Definition | df-leag 27586* | Definition of the geometrical "angle less than" relation. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.) |
β’ β€β = (π β V β¦ {β¨π, πβ© β£ ((π β ((Baseβπ) βm (0..^3)) β§ π β ((Baseβπ) βm (0..^3))) β§ βπ₯ β (Baseβπ)(π₯(inAβπ)β¨β(πβ0)(πβ1)(πβ2)ββ© β§ β¨β(πβ0)(πβ1)(πβ2)ββ©(cgrAβπ)β¨β(πβ0)(πβ1)π₯ββ©))}) | ||
Theorem | isleag 27587* | Geometrical "less than" property for angles. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π (π₯(inAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπ₯ββ©))) | ||
Theorem | isleagd 27588 | Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ β€ = (β€β βπΊ) & β’ (π β π β π) & β’ (π β π(inAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) β β’ (π β β¨βπ΄π΅πΆββ© β€ β¨βπ·πΈπΉββ©) | ||
Theorem | leagne1 27589 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | leagne2 27590 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΆ β π΅) | ||
Theorem | leagne3 27591 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π· β πΈ) | ||
Theorem | leagne4 27592 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΉ β πΈ) | ||
Theorem | cgrg3col4 27593* | Lemma 11.28 of [Schwabhauser] p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ πΏ = (LineGβπΊ) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β (π β (π΄πΏπΆ) β¨ π΄ = πΆ)) β β’ (π β βπ¦ β π β¨βπ΄π΅πΆπββ©(cgrGβπΊ)β¨βπ·πΈπΉπ¦ββ©) | ||
Theorem | tgsas1 27594 | First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then third sides are equal in length. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) β β’ (π β (πΆ β π΄) = (πΉ β π·)) | ||
Theorem | tgsas 27595 | First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then the triangles are congruent. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) β β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | tgsas2 27596 | First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β π΄ β πΆ) β β’ (π β β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ©) | ||
Theorem | tgsas3 27597 | First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β π΄ β πΆ) β β’ (π β β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©) | ||
Theorem | tgasa1 27598 | Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ©) β β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) | ||
Theorem | tgasa 27599 | Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ©) β β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | tgsss1 27600 | Third congruence theorem: SSS (Side-Side-Side): If the three pairs of sides of two triangles are equal in length, then the triangles are congruent. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β (πΆ β π΄) = (πΉ β π·)) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |