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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | clmi 27501 | Declare the constant for the line mirroring function. |
class lInvG | ||
Definition | df-mid 27502* | Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 27506, midbtwn 27507, and midcgr 27508. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
β’ midG = (π β V β¦ (π β (Baseβπ), π β (Baseβπ) β¦ (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ)))) | ||
Definition | df-lmi 27503* | Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 27515. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ lInvG = (π β V β¦ (π β ran (LineGβπ) β¦ (π β (Baseβπ) β¦ (β©π β (Baseβπ)((π(midGβπ)π) β π β§ (π(βGβπ)(π(LineGβπ)π) β¨ π = π)))))) | ||
Theorem | midf 27504 | Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β (midGβπΊ):(π Γ π)βΆπ) | ||
Theorem | midcl 27505 | Closure of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β π) | ||
Theorem | ismidb 27506 | Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (pInvGβπΊ) & β’ (π β π β π) β β’ (π β (π΅ = ((πβπ)βπ΄) β (π΄(midGβπΊ)π΅) = π)) | ||
Theorem | midbtwn 27507 | Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) β (π΄πΌπ΅)) | ||
Theorem | midcgr 27508 | Congruence of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄(midGβπΊ)π΅) = πΆ) β β’ (π β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | midid 27509 | Midpoint of a null segment. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΄) = π΄) | ||
Theorem | midcom 27510 | Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(midGβπΊ)π΅) = (π΅(midGβπΊ)π΄)) | ||
Theorem | mirmid 27511 | Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ (π β π β π) β β’ (π β ((πβπ΄)(midGβπΊ)(πβπ΅)) = (πβ(π΄(midGβπΊ)π΅))) | ||
Theorem | lmieu 27512* | 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 27513 | Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) β β’ (π β π:πβΆπ) | ||
Theorem | lmicl 27514 | Closure of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β π) | ||
Theorem | islmib 27515 | 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 27516 | 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 27517 | 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 27518* | 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 27519 | 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 27520 | 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 27521 | The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΄ β π·) β β’ (π β (πβπ΄) = π΄) | ||
Theorem | lmimid 27522 | 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 27523 | 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 27524 | Lemma for lmiiso 27525. (Contributed by Thierry Arnoux, 14-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β πΊDimTarskiGβ₯2) & β’ π = ((lInvGβπΊ)βπ·) & β’ πΏ = (LineGβπΊ) & β’ (π β π· β ran πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = ((pInvGβπΊ)βπ) & β’ π = ((π΄(midGβπΊ)(πβπ΄))(midGβπΊ)(π΅(midGβπΊ)(πβπ΅))) β β’ (π β ((πβπ΄) β (πβπ΅)) = (π΄ β π΅)) | ||
Theorem | lmiiso 27525 | 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 27526 | 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 27527 | Lemma for hypcgr 27529, 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 27528 | Lemma for hypcgr 27529, 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 27529 | 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 27530* | 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 27531* | 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 27532* | 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 27533* | Lemma for trgcopyeu 27534. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) & β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ π = {β¨π, πβ© β£ ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))} & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) & β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β’ (π β π = π) | ||
Theorem | trgcopyeu 27534* | 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 27535 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 27536* | Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 27537 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 27537* | 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 27558 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ))) | ||
Theorem | iscgra1 27538* | A special version of iscgra 27537 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 27539 | Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βππΈπββ©) & β’ (π β π(πΎβπΈ)π·) & β’ (π β π(πΎβπΈ)πΉ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgrane1 27540 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | cgrane2 27541 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΅ β πΆ) | ||
Theorem | cgrane3 27542 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β π·) | ||
Theorem | cgrane4 27543 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β πΉ) | ||
Theorem | cgrahl1 27544 | 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 27545 | 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 27546 | 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 27547 | 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 27548 | 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 27549 | 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 27550 | 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 27551 | 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 27552 | Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΉ)) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π· β πΈ) & β’ (π β πΉ β πΈ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgraswaplr 27553 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β β¨βπΆπ΅π΄ββ©(cgrAβπΊ)β¨βπΉπΈπ·ββ©) | ||
Theorem | cgrabtwn 27554 | 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 27555 | 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 27556 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | cgrancol 27557 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β Β¬ (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | dfcgra2 27558* | 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 27536 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β ((π΄ β π΅ β§ πΆ β π΅) β§ (π· β πΈ β§ πΉ β πΈ) β§ βπ β π βπ β π βπ β π βπ β π (((π΄ β (π΅πΌπ) β§ (π΄ β π) = (πΈ β π·)) β§ (πΆ β (π΅πΌπ) β§ (πΆ β π) = (πΈ β πΉ))) β§ ((π· β (πΈπΌπ) β§ (π· β π) = (π΅ β π΄)) β§ (πΉ β (πΈπΌπ) β§ (πΉ β π) = (π΅ β πΆ))) β§ (π β π) = (π β π))))) | ||
Theorem | sacgr 27559 | 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 27560 | 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 27561* | 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 27562 | 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 27563 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 27564 | Extend class relation with the "angle less than" relation. |
class β€β | ||
Definition | df-inag 27565* | 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 27566* | 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 27567 | Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π β (π΄πΌπΆ)) & β’ (π β (π = π΅ β¨ π(πΎβπ΅)π)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagflat 27568 | Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagswap 27569 | 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 27570 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π΄ β π΅) | ||
Theorem | inagne2 27571 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β πΆ β π΅) | ||
Theorem | inagne3 27572 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π β π΅) | ||
Theorem | inaghl 27573 | 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 27574* | 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 27575* | 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 27576 | Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ β€ = (β€β βπΊ) & β’ (π β π β π) & β’ (π β π(inAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) β β’ (π β β¨βπ΄π΅πΆββ© β€ β¨βπ·πΈπΉββ©) | ||
Theorem | leagne1 27577 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | leagne2 27578 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΆ β π΅) | ||
Theorem | leagne3 27579 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π· β πΈ) | ||
Theorem | leagne4 27580 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΉ β πΈ) | ||
Theorem | cgrg3col4 27581* | 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 27582 | 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 27583 | 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 27584 | 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 27585 | 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 27586 | 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 27587 | 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 27588 | 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βπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | tgsss2 27589 | Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β (πΆ β π΄) = (πΉ β π·)) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) β β’ (π β β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ©) | ||
Theorem | tgsss3 27590 | Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β (πΆ β π΄) = (πΉ β π·)) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) β β’ (π β β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©) | ||
Theorem | dfcgrg2 27591 | Congruence for two triangles can also be defined as congruence of sides and angles (6 parts). This is often the actual textbook definition of triangle congruence, see for example https://en.wikipedia.org/wiki/Congruence_(geometry)#Congruence_of_triangles. With this definition, the "SSS" congruence theorem has an additional part, namely, that triangle congruence implies congruence of the sides (which means equality of the lengths). Because our development of elementary geometry strives to closely follow Schwabhaeuser's, our original definition of shape congruence, df-cgrg 27239, already covers that part: see trgcgr 27244. This theorem is also named "CPCTC", which stands for "Corresponding Parts of Congruent Triangles are Congruent", see https://en.wikipedia.org/wiki/Congruence_(geometry)#CPCTC 27244. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β (((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)) β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)))) | ||
Theorem | isoas 27592 | Congruence theorem for isocele triangles: if two angles of a triangle are congruent, then the corresponding sides also are. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ΄πΆπ΅ββ©) β β’ (π β (π΄ β π΅) = (π΄ β πΆ)) | ||
Syntax | ceqlg 27593 | Declare the class of equilateral triangles. |
class eqltrG | ||
Definition | df-eqlg 27594* | Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
β’ eqltrG = (π β V β¦ {π₯ β ((Baseβπ) βm (0..^3)) β£ π₯(cgrGβπ)β¨β(π₯β1)(π₯β2)(π₯β0)ββ©}) | ||
Theorem | iseqlg 27595 | Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β (β¨βπ΄π΅πΆββ© β (eqltrGβπΊ) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ΅πΆπ΄ββ©)) | ||
Theorem | iseqlgd 27596 | Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π΄ β π΅) = (π΅ β πΆ)) & β’ (π β (π΅ β πΆ) = (πΆ β π΄)) & β’ (π β (πΆ β π΄) = (π΄ β π΅)) β β’ (π β β¨βπ΄π΅πΆββ© β (eqltrGβπΊ)) | ||
Theorem | f1otrgds 27597* | Convenient lemma for f1otrg 27599. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) | ||
Theorem | f1otrgitv 27598* | Convenient lemma for f1otrg 27599. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) | ||
Theorem | f1otrg 27599* | A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π» β π) & β’ (π β πΊ β TarskiG) & β’ (π β (LineGβπ») = (π₯ β π΅, π¦ β (π΅ β {π₯}) β¦ {π§ β π΅ β£ (π§ β (π₯π½π¦) β¨ π₯ β (π§π½π¦) β¨ π¦ β (π₯π½π§))})) β β’ (π β π» β TarskiG) | ||
Theorem | f1otrge 27600* | A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π» β π) & β’ (π β πΊ β TarskiGE) β β’ (π β π» β TarskiGE) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |