![]() |
Metamath
Proof Explorer Theorem List (p. 287 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-hpg 28601* | Define the open half plane relation for a geometry πΊ. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 28603 to find the same formulation. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ hpG = (π β V β¦ (π β ran (LineGβπ) β¦ {β¨π, πβ© β£ [(Baseβπ) / π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)))})) | ||
Theorem | ishpg 28602* | 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 28603* | 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 28604* | 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 28605* | 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 28606* | Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} & β’ (π β πΊ β TarskiG) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ππΆ) β β’ (π β (π΅ππΆ β π΄((hpGβπΊ)βπ·)π΅)) | ||
Theorem | lnoppnhpg 28607* | 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 28608* | 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 28609* | 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 28610* | 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 28611* | 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 28612* | 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 28613* | 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 28614* | 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 28615 | Declare the constant for the midpoint operation. |
class midG | ||
Syntax | clmi 28616 | Declare the constant for the line mirroring function. |
class lInvG | ||
Definition | df-mid 28617* | Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 28621, midbtwn 28622, and midcgr 28623. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
β’ midG = (π β V β¦ (π β (Baseβπ), π β (Baseβπ) β¦ (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ)))) | ||
Definition | df-lmi 28618* | Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 28630. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ lInvG = (π β V β¦ (π β ran (LineGβπ) β¦ (π β (Baseβπ) β¦ (β©π β (Baseβπ)((π(midGβπ)π) β π β§ (π(βGβπ)(π(LineGβπ)π) β¨ π = π)))))) | ||
Theorem | midf 28619 | Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β (midGβπΊ):(π Γ π)βΆπ) | ||
Theorem | midcl 28620 | Closure of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β π) | ||
Theorem | ismidb 28621 | Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (pInvGβπΊ) & β’ (π β π β π) β β’ (π β (π΅ = ((πβπ)βπ΄) β (π΄(midGβπΊ)π΅) = π)) | ||
Theorem | midbtwn 28622 | Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β (π΄πΌπ΅)) | ||
Theorem | midcgr 28623 | Congruence of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄(midGβπΊ)π΅) = πΆ) β β’ (π β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | midid 28624 | Midpoint of a null segment. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΄) = π΄) | ||
Theorem | midcom 28625 | Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) = (π΅(midGβπΊ)π΄)) | ||
Theorem | mirmid 28626 | Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π β π) β β’ (π β ((πβπ΄)(midGβπΊ)(πβπ΅)) = (πβ(π΄(midGβπΊ)π΅))) | ||
Theorem | lmieu 28627* | 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 28628 | Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) β β’ (π β π:πβΆπ) | ||
Theorem | lmicl 28629 | Closure of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β π) | ||
Theorem | islmib 28630 | 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 28631 | 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 28632 | 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 28633* | 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 28634 | 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 28635 | 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 28636 | The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΄ β π·) β β’ (π β (πβπ΄) = π΄) | ||
Theorem | lmimid 28637 | 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 28638 | 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 28639 | Lemma for lmiiso 28640. (Contributed by Thierry Arnoux, 14-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ π = ((π΄(midGβπΊ)(πβπ΄))(midGβπΊ)(π΅(midGβπΊ)(πβπ΅))) β β’ (π β ((πβπ΄) β (πβπ΅)) = (π΄ β π΅)) | ||
Theorem | lmiiso 28640 | 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 28641 | 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 28642 | Lemma for hypcgr 28644, 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 28643 | Lemma for hypcgr 28644, 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 28644 | 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 28645* | 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 28646* | 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 28647* | 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 28648* | Lemma for trgcopyeu 28649. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ π = {β¨π, πβ© β£ ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))} & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β’ (π β π = π) | ||
Theorem | trgcopyeu 28649* | 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 28650 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 28651* | Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 28652 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 28652* | 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 28673 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ))) | ||
Theorem | iscgra1 28653* | A special version of iscgra 28652 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 28654 | Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βππΈπββ©) & β’ (π β π(πΎβπΈ)π·) & β’ (π β π(πΎβπΈ)πΉ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgrane1 28655 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | cgrane2 28656 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΅ β πΆ) | ||
Theorem | cgrane3 28657 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β π·) | ||
Theorem | cgrane4 28658 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β πΉ) | ||
Theorem | cgrahl1 28659 | 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 28660 | 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 28661 | 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 28662 | 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 28663 | 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 28664 | 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 28665 | 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 28666 | 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 28667 | Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΉ)) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π· β πΈ) & β’ (π β πΉ β πΈ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgraswaplr 28668 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β β¨βπΆπ΅π΄ββ©(cgrAβπΊ)β¨βπΉπΈπ·ββ©) | ||
Theorem | cgrabtwn 28669 | 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 28670 | 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 28671 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | cgrancol 28672 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β Β¬ (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | dfcgra2 28673* | 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 28651 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β ((π΄ β π΅ β§ πΆ β π΅) β§ (π· β πΈ β§ πΉ β πΈ) β§ βπ β π βπ β π βπ β π βπ β π (((π΄ β (π΅πΌπ) β§ (π΄ β π) = (πΈ β π·)) β§ (πΆ β (π΅πΌπ) β§ (πΆ β π) = (πΈ β πΉ))) β§ ((π· β (πΈπΌπ) β§ (π· β π) = (π΅ β π΄)) β§ (πΉ β (πΈπΌπ) β§ (πΉ β π) = (π΅ β πΆ))) β§ (π β π) = (π β π))))) | ||
Theorem | sacgr 28674 | 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 28675 | 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 28676* | 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 28677 | 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 28678 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 28679 | Extend class relation with the "angle less than" relation. |
class β€β | ||
Definition | df-inag 28680* | 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 28681* | 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 28682 | Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π β (π΄πΌπΆ)) & β’ (π β (π = π΅ β¨ π(πΎβπ΅)π)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagflat 28683 | Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagswap 28684 | 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 28685 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π΄ β π΅) | ||
Theorem | inagne2 28686 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β πΆ β π΅) | ||
Theorem | inagne3 28687 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π β π΅) | ||
Theorem | inaghl 28688 | 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 28689* | 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 28690* | 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 28691 | Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ β€ = (β€β βπΊ) & β’ (π β π β π) & β’ (π β π(inAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) β β’ (π β β¨βπ΄π΅πΆββ© β€ β¨βπ·πΈπΉββ©) | ||
Theorem | leagne1 28692 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | leagne2 28693 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΆ β π΅) | ||
Theorem | leagne3 28694 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π· β πΈ) | ||
Theorem | leagne4 28695 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΉ β πΈ) | ||
Theorem | cgrg3col4 28696* | 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 28697 | 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 28698 | 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 28699 | 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 28700 | First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β π΄ β πΆ) β β’ (π β β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |