![]() |
Metamath
Proof Explorer Theorem List (p. 282 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | leagne2 28101 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΆ β π΅) | ||
Theorem | leagne3 28102 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π· β πΈ) | ||
Theorem | leagne4 28103 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΉ β πΈ) | ||
Theorem | cgrg3col4 28104* | 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 28105 | 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 28106 | 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 28107 | 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 28108 | 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 28109 | 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 28110 | 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 28111 | 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 28112 | 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 28113 | 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 28114 | 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 27762, already covers that part: see trgcgr 27767. 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 27767. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β (((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)) β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)))) | ||
Theorem | isoas 28115 | 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 28116 | Declare the class of equilateral triangles. |
class eqltrG | ||
Definition | df-eqlg 28117* | 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 28118 | Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β (β¨βπ΄π΅πΆββ© β (eqltrGβπΊ) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ΅πΆπ΄ββ©)) | ||
Theorem | iseqlgd 28119 | Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π΄ β π΅) = (π΅ β πΆ)) & β’ (π β (π΅ β πΆ) = (πΆ β π΄)) & β’ (π β (πΆ β π΄) = (π΄ β π΅)) β β’ (π β β¨βπ΄π΅πΆββ© β (eqltrGβπΊ)) | ||
Theorem | f1otrgds 28120* | Convenient lemma for f1otrg 28122. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) | ||
Theorem | f1otrgitv 28121* | Convenient lemma for f1otrg 28122. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) | ||
Theorem | f1otrg 28122* | 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 28123* | 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) | ||
Syntax | cttg 28124 | Function to convert an algebraic structure to a Tarski geometry. |
class toTG | ||
Definition | df-ttg 28125* | Define a function converting a subcomplex Hilbert space to a Tarski Geometry. It does so by equipping the structure with a betweenness operation. Note that because the scalar product is applied over the interval (0[,]1), only spaces whose scalar field is a superset of that interval can be considered. (Contributed by Thierry Arnoux, 24-Mar-2019.) |
β’ toTG = (π€ β V β¦ β¦(π₯ β (Baseβπ€), π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ βπ β (0[,]1)(π§(-gβπ€)π₯) = (π( Β·π βπ€)(π¦(-gβπ€)π₯))}) / πβ¦((π€ sSet β¨(Itvβndx), πβ©) sSet β¨(LineGβndx), (π₯ β (Baseβπ€), π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})β©)) | ||
Theorem | ttgval 28126* | Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof shortened by AV, 9-Nov-2024.) |
β’ πΊ = (toTGβπ») & β’ π΅ = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») & β’ πΌ = (ItvβπΊ) β β’ (π» β π β (πΊ = ((π» sSet β¨(Itvβndx), (π₯ β π΅, π¦ β π΅ β¦ {π§ β π΅ β£ βπ β (0[,]1)(π§ β π₯) = (π Β· (π¦ β π₯))})β©) sSet β¨(LineGβndx), (π₯ β π΅, π¦ β π΅ β¦ {π§ β π΅ β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})β©) β§ πΌ = (π₯ β π΅, π¦ β π΅ β¦ {π§ β π΅ β£ βπ β (0[,]1)(π§ β π₯) = (π Β· (π¦ β π₯))}))) | ||
Theorem | ttgvalOLD 28127* | Obsolete proof of ttgval 28126 as of 9-Nov-2024. Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ π΅ = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») & β’ πΌ = (ItvβπΊ) β β’ (π» β π β (πΊ = ((π» sSet β¨(Itvβndx), (π₯ β π΅, π¦ β π΅ β¦ {π§ β π΅ β£ βπ β (0[,]1)(π§ β π₯) = (π Β· (π¦ β π₯))})β©) sSet β¨(LineGβndx), (π₯ β π΅, π¦ β π΅ β¦ {π§ β π΅ β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})β©) β§ πΌ = (π₯ β π΅, π¦ β π΅ β¦ {π§ β π΅ β£ βπ β (0[,]1)(π§ β π₯) = (π Β· (π¦ β π₯))}))) | ||
Theorem | ttglem 28128 | Lemma for ttgbas 28130, ttgvsca 28135 etc. (Contributed by Thierry Arnoux, 15-Apr-2019.) (Revised by AV, 29-Oct-2024.) |
β’ πΊ = (toTGβπ») & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (LineGβndx) & β’ (πΈβndx) β (Itvβndx) β β’ (πΈβπ») = (πΈβπΊ) | ||
Theorem | ttglemOLD 28129 | Obsolete version of ttglem 28128 as of 29-Oct-2024. Lemma for ttgbas 28130 and ttgvsca 28135. (Contributed by Thierry Arnoux, 15-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ πΈ = Slot π & β’ π β β & β’ π < ;16 β β’ (πΈβπ») = (πΈβπΊ) | ||
Theorem | ttgbas 28130 | The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.) |
β’ πΊ = (toTGβπ») & β’ π΅ = (Baseβπ») β β’ π΅ = (BaseβπΊ) | ||
Theorem | ttgbasOLD 28131 | Obsolete proof of ttgbas 28130 as of 29-Oct-2024. The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ π΅ = (Baseβπ») β β’ π΅ = (BaseβπΊ) | ||
Theorem | ttgplusg 28132 | The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.) |
β’ πΊ = (toTGβπ») & β’ + = (+gβπ») β β’ + = (+gβπΊ) | ||
Theorem | ttgplusgOLD 28133 | Obsolete proof of ttgplusg 28132 as of 29-Oct-2024. The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ + = (+gβπ») β β’ + = (+gβπΊ) | ||
Theorem | ttgsub 28134 | The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ β = (-gβπ») β β’ β = (-gβπΊ) | ||
Theorem | ttgvsca 28135 | The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.) |
β’ πΊ = (toTGβπ») & β’ Β· = ( Β·π βπ») β β’ Β· = ( Β·π βπΊ) | ||
Theorem | ttgvscaOLD 28136 | Obsolete proof of ttgvsca 28135 as of 29-Oct-2024. The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ Β· = ( Β·π βπ») β β’ Β· = ( Β·π βπΊ) | ||
Theorem | ttgds 28137 | The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.) |
β’ πΊ = (toTGβπ») & β’ π· = (distβπ») β β’ π· = (distβπΊ) | ||
Theorem | ttgdsOLD 28138 | Obsolete proof of ttgds 28137 as of 29-Oct-2024. The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ π· = (distβπ») β β’ π· = (distβπΊ) | ||
Theorem | ttgitvval 28139* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») β β’ ((π» β π β§ π β π β§ π β π) β (ππΌπ) = {π§ β π β£ βπ β (0[,]1)(π§ β π) = (π Β· (π β π))}) | ||
Theorem | ttgelitv 28140* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π» β π) & β’ (π β π β π) β β’ (π β (π β (ππΌπ) β βπ β (0[,]1)(π β π) = (π Β· (π β π)))) | ||
Theorem | ttgbtwnid 28141 | Any subcomplex module equipped with the betweenness operation fulfills the identity of betweenness (Axiom A6). (Contributed by Thierry Arnoux, 26-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») & β’ (π β π β π) & β’ (π β π β π) & β’ π = (Baseβ(Scalarβπ»)) & β’ (π β (0[,]1) β π ) & β’ (π β π» β βMod) & β’ (π β π β (ππΌπ)) β β’ (π β π = π) | ||
Theorem | ttgcontlem1 28142 | Lemma for % ttgcont . (Contributed by Thierry Arnoux, 24-May-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») & β’ (π β π β π) & β’ (π β π β π) & β’ π = (Baseβ(Scalarβπ»)) & β’ (π β (0[,]1) β π ) & β’ + = (+gβπ») & β’ (π β π» β βVec) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β π β 0) & β’ (π β πΎ β 0) & β’ (π β πΎ β 1) & β’ (π β πΏ β π) & β’ (π β πΏ β€ (π / πΎ)) & β’ (π β πΏ β (0[,]1)) & β’ (π β πΎ β (0[,]1)) & β’ (π β π β (0[,]πΏ)) & β’ (π β (π β π΄) = (πΎ Β· (π β π΄))) & β’ (π β (π β π΄) = (π Β· (π β π΄))) & β’ (π β π΅ = (π΄ + (πΏ Β· (π β π΄)))) β β’ (π β π΅ β (ππΌπ)) | ||
Theorem | xmstrkgc 28143 | Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.) |
β’ (πΊ β βMetSp β πΊ β TarskiGC) | ||
Theorem | cchhllem 28144* | Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019.) (Revised by AV, 29-Oct-2024.) |
β’ πΆ = (((subringAlg ββfld)ββ) sSet β¨(Β·πβndx), (π₯ β β, π¦ β β β¦ (π₯ Β· (ββπ¦)))β©) & β’ πΈ = Slot (πΈβndx) & β’ (Scalarβndx) β (πΈβndx) & β’ ( Β·π βndx) β (πΈβndx) & β’ (Β·πβndx) β (πΈβndx) β β’ (πΈββfld) = (πΈβπΆ) | ||
Theorem | cchhllemOLD 28145* | Obsolete version of cchhllem 28144 as of 29-Oct-2024. Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΆ = (((subringAlg ββfld)ββ) sSet β¨(Β·πβndx), (π₯ β β, π¦ β β β¦ (π₯ Β· (ββπ¦)))β©) & β’ πΈ = Slot π & β’ π β β & β’ (π < 5 β¨ 8 < π) β β’ (πΈββfld) = (πΈβπΆ) | ||
Syntax | cee 28146 | Declare the syntax for the Euclidean space generator. |
class πΌ | ||
Syntax | cbtwn 28147 | Declare the syntax for the Euclidean betweenness predicate. |
class Btwn | ||
Syntax | ccgr 28148 | Declare the syntax for the Euclidean congruence predicate. |
class Cgr | ||
Definition | df-ee 28149 | Define the Euclidean space generator. For details, see elee 28152. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ πΌ = (π β β β¦ (β βm (1...π))) | ||
Definition | df-btwn 28150* | Define the Euclidean betweenness predicate. For details, see brbtwn 28157. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ Btwn = β‘{β¨β¨π₯, π§β©, π¦β© β£ βπ β β ((π₯ β (πΌβπ) β§ π§ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ βπ‘ β (0[,]1)βπ β (1...π)(π¦βπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π§βπ))))} | ||
Definition | df-cgr 28151* | Define the Euclidean congruence predicate. For details, see brcgr 28158. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ Cgr = {β¨π₯, π¦β© β£ βπ β β ((π₯ β ((πΌβπ) Γ (πΌβπ)) β§ π¦ β ((πΌβπ) Γ (πΌβπ))) β§ Ξ£π β (1...π)((((1st βπ₯)βπ) β ((2nd βπ₯)βπ))β2) = Ξ£π β (1...π)((((1st βπ¦)βπ) β ((2nd βπ¦)βπ))β2))} | ||
Theorem | elee 28152 | Membership in a Euclidean space. We define Euclidean space here using Cartesian coordinates over π space. We later abstract away from this using Tarski's geometry axioms, so this exact definition is unimportant. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ (π β β β (π΄ β (πΌβπ) β π΄:(1...π)βΆβ)) | ||
Theorem | mptelee 28153* | A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.) |
β’ (π β β β ((π β (1...π) β¦ (π΄πΉπ΅)) β (πΌβπ) β βπ β (1...π)(π΄πΉπ΅) β β)) | ||
Theorem | eleenn 28154 | If π΄ is in (πΌβπ), then π is a natural. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ (π΄ β (πΌβπ) β π β β) | ||
Theorem | eleei 28155 | The forward direction of elee 28152. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ (π΄ β (πΌβπ) β π΄:(1...π)βΆβ) | ||
Theorem | eedimeq 28156 | A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΄ β (πΌβπ)) β π = π) | ||
Theorem | brbtwn 28157* | The binary relation form of the betweenness predicate. The statement π΄ Btwn β¨π΅, πΆβ© should be informally read as "π΄ lies on a line segment between π΅ and πΆ. This exact definition is abstracted away by Tarski's geometry axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β (π΄ Btwn β¨π΅, πΆβ© β βπ‘ β (0[,]1)βπ β (1...π)(π΄βπ) = (((1 β π‘) Β· (π΅βπ)) + (π‘ Β· (πΆβπ))))) | ||
Theorem | brcgr 28158* | The binary relation form of the congruence predicate. The statement β¨π΄, π΅β©Cgrβ¨πΆ, π·β© should be read informally as "the π dimensional point π΄ is as far from π΅ as πΆ is from π·, or "the line segment π΄π΅ is congruent to the line segment πΆπ·. This particular definition is encapsulated by Tarski's axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) = Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2))) | ||
Theorem | fveere 28159 | The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ πΌ β (1...π)) β (π΄βπΌ) β β) | ||
Theorem | fveecn 28160 | The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ πΌ β (1...π)) β (π΄βπΌ) β β) | ||
Theorem | eqeefv 28161* | Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (π΄ = π΅ β βπ β (1...π)(π΄βπ) = (π΅βπ))) | ||
Theorem | eqeelen 28162* | Two points are equal iff the square of the distance between them is zero. (Contributed by Scott Fenton, 10-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (π΄ = π΅ β Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) = 0)) | ||
Theorem | brbtwn2 28163* | Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β (π΄ Btwn β¨π΅, πΆβ© β (βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) β€ 0 β§ βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ)))))) | ||
Theorem | colinearalglem1 28164 | Lemma for colinearalg 28168. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π· β β β§ πΈ β β β§ πΉ β β)) β (((π΅ β π΄) Β· (πΉ β π·)) = ((πΈ β π·) Β· (πΆ β π΄)) β ((π΅ Β· πΉ) β ((π΄ Β· πΉ) + (π΅ Β· π·))) = ((πΆ Β· πΈ) β ((π΄ Β· πΈ) + (πΆ Β· π·))))) | ||
Theorem | colinearalglem2 28165* | Lemma for colinearalg 28168. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β (βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) β βπ β (1...π)βπ β (1...π)(((πΆβπ) β (π΅βπ)) Β· ((π΄βπ) β (π΅βπ))) = (((πΆβπ) β (π΅βπ)) Β· ((π΄βπ) β (π΅βπ))))) | ||
Theorem | colinearalglem3 28166* | Lemma for colinearalg 28168. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β (βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) β βπ β (1...π)βπ β (1...π)(((π΄βπ) β (πΆβπ)) Β· ((π΅βπ) β (πΆβπ))) = (((π΄βπ) β (πΆβπ)) Β· ((π΅βπ) β (πΆβπ))))) | ||
Theorem | colinearalglem4 28167* | Lemma for colinearalg 28168. Prove a disjunction that will be needed in the final proof. (Contributed by Scott Fenton, 27-Jun-2013.) |
β’ (((π΄ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ πΎ β β) β (βπ β (1...π)((((πΎ Β· ((πΆβπ) β (π΄βπ))) + (π΄βπ)) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) β€ 0 β¨ βπ β (1...π)(((πΆβπ) β ((πΎ Β· ((πΆβπ) β (π΄βπ))) + (π΄βπ))) Β· ((π΄βπ) β ((πΎ Β· ((πΆβπ) β (π΄βπ))) + (π΄βπ)))) β€ 0 β¨ βπ β (1...π)(((π΄βπ) β (πΆβπ)) Β· (((πΎ Β· ((πΆβπ) β (π΄βπ))) + (π΄βπ)) β (πΆβπ))) β€ 0)) | ||
Theorem | colinearalg 28168* | An algebraic characterization of colinearity. Note the similarity to brbtwn2 28163. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β ((π΄ Btwn β¨π΅, πΆβ© β¨ π΅ Btwn β¨πΆ, π΄β© β¨ πΆ Btwn β¨π΄, π΅β©) β βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))))) | ||
Theorem | eleesub 28169* | Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.) |
β’ πΆ = (π β (1...π) β¦ ((π΄βπ) β (π΅βπ))) β β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β πΆ β (πΌβπ)) | ||
Theorem | eleesubd 28170* | Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 28169. (Contributed by Scott Fenton, 17-Jul-2013.) |
β’ (π β πΆ = (π β (1...π) β¦ ((π΄βπ) β (π΅βπ)))) β β’ ((π β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β πΆ β (πΌβπ)) | ||
Theorem | axdimuniq 28171 | The unique dimension axiom. If a point is in π dimensional space and in π dimensional space, then π = π. This axiom is not traditionally presented with Tarski's axioms, but we require it here as we are considering spaces in arbitrary dimensions. (Contributed by Scott Fenton, 24-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ)) β§ (π β β β§ π΄ β (πΌβπ))) β π = π) | ||
Theorem | axcgrrflx 28172 | π΄ is as far from π΅ as π΅ is from π΄. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΅β©Cgrβ¨π΅, π΄β©) | ||
Theorem | axcgrtr 28173 | Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©)) | ||
Theorem | axcgrid 28174 | If there is no distance between π΄ and π΅, then π΄ = π΅. Axiom A3 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, πΆβ© β π΄ = π΅)) | ||
Theorem | axsegconlem1 28175* | Lemma for axsegcon 28185. Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013.) |
β’ ((π΄ = π΅ β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)))) β βπ₯ β (πΌβπ)βπ‘ β (0[,]1)(βπ β (1...π)(π΅βπ) = (((1 β π‘) Β· (π΄βπ)) + (π‘ Β· (π₯βπ))) β§ Ξ£π β (1...π)(((π΅βπ) β (π₯βπ))β2) = Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2))) | ||
Theorem | axsegconlem2 28176* | Lemma for axsegcon 28185. Show that the square of the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) β β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π β β) | ||
Theorem | axsegconlem3 28177* | Lemma for axsegcon 28185. Show that the square of the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) β β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β 0 β€ π) | ||
Theorem | axsegconlem4 28178* | Lemma for axsegcon 28185. Show that the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) β β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (ββπ) β β) | ||
Theorem | axsegconlem5 28179* | Lemma for axsegcon 28185. Show that the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) β β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β 0 β€ (ββπ)) | ||
Theorem | axsegconlem6 28180* | Lemma for axsegcon 28185. Show that the distance between two distinct points is positive. (Contributed by Scott Fenton, 17-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) β β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β 0 < (ββπ)) | ||
Theorem | axsegconlem7 28181* | Lemma for axsegcon 28185. Show that a particular ratio of distances is in the closed unit interval. (Contributed by Scott Fenton, 18-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) & β’ π = Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2) β β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((ββπ) / ((ββπ) + (ββπ))) β (0[,]1)) | ||
Theorem | axsegconlem8 28182* | Lemma for axsegcon 28185. Show that a particular mapping generates a point. (Contributed by Scott Fenton, 18-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) & β’ π = Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2) & β’ πΉ = (π β (1...π) β¦ (((((ββπ) + (ββπ)) Β· (π΅βπ)) β ((ββπ) Β· (π΄βπ))) / (ββπ))) β β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β πΉ β (πΌβπ)) | ||
Theorem | axsegconlem9 28183* | Lemma for axsegcon 28185. Show that π΅πΉ is congruent to πΆπ·. (Contributed by Scott Fenton, 19-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) & β’ π = Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2) & β’ πΉ = (π β (1...π) β¦ (((((ββπ) + (ββπ)) Β· (π΅βπ)) β ((ββπ) Β· (π΄βπ))) / (ββπ))) β β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β Ξ£π β (1...π)(((π΅βπ) β (πΉβπ))β2) = Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2)) | ||
Theorem | axsegconlem10 28184* | Lemma for axsegcon 28185. Show that the scaling constant from axsegconlem7 28181 produces the betweenness condition for π΄, π΅ and πΉ. (Contributed by Scott Fenton, 21-Sep-2013.) |
β’ π = Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) & β’ π = Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2) & β’ πΉ = (π β (1...π) β¦ (((((ββπ) + (ββπ)) Β· (π΅βπ)) β ((ββπ) Β· (π΄βπ))) / (ββπ))) β β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β βπ β (1...π)(π΅βπ) = (((1 β ((ββπ) / ((ββπ) + (ββπ)))) Β· (π΄βπ)) + (((ββπ) / ((ββπ) + (ββπ))) Β· (πΉβπ)))) | ||
Theorem | axsegcon 28185* | Any segment π΄π΅ can be extended to a point π₯ such that π΅π₯ is congruent to πΆπ·. Axiom A4 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 4-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β βπ₯ β (πΌβπ)(π΅ Btwn β¨π΄, π₯β© β§ β¨π΅, π₯β©Cgrβ¨πΆ, π·β©)) | ||
Theorem | ax5seglem1 28186* | Lemma for ax5seg 28196. Rexpress a one congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π β (0[,]1) β§ βπ β (1...π)(π΅βπ) = (((1 β π) Β· (π΄βπ)) + (π Β· (πΆβπ))))) β Ξ£π β (1...π)(((π΄βπ) β (π΅βπ))β2) = ((πβ2) Β· Ξ£π β (1...π)(((π΄βπ) β (πΆβπ))β2))) | ||
Theorem | ax5seglem2 28187* | Lemma for ax5seg 28196. Rexpress another congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π β (0[,]1) β§ βπ β (1...π)(π΅βπ) = (((1 β π) Β· (π΄βπ)) + (π Β· (πΆβπ))))) β Ξ£π β (1...π)(((π΅βπ) β (πΆβπ))β2) = (((1 β π)β2) Β· Ξ£π β (1...π)(((π΄βπ) β (πΆβπ))β2))) | ||
Theorem | ax5seglem3a 28188 | Lemma for ax5seg 28196. (Contributed by Scott Fenton, 7-May-2015.) |
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ π β (1...π)) β (((π΄βπ) β (πΆβπ)) β β β§ ((π·βπ) β (πΉβπ)) β β)) | ||
Theorem | ax5seglem3 28189* | Lemma for ax5seg 28196. Combine congruences for points on a line. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ ((π β (0[,]1) β§ π β (0[,]1)) β§ (βπ β (1...π)(π΅βπ) = (((1 β π) Β· (π΄βπ)) + (π Β· (πΆβπ))) β§ βπ β (1...π)(πΈβπ) = (((1 β π) Β· (π·βπ)) + (π Β· (πΉβπ))))) β§ (β¨π΄, π΅β©Cgrβ¨π·, πΈβ© β§ β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©)) β Ξ£π β (1...π)(((π΄βπ) β (πΆβπ))β2) = Ξ£π β (1...π)(((π·βπ) β (πΉβπ))β2)) | ||
Theorem | ax5seglem4 28190* | Lemma for ax5seg 28196. Given two distinct points, the scaling constant in a betweenness statement is nonzero. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ βπ β (1...π)(π΅βπ) = (((1 β π) Β· (π΄βπ)) + (π Β· (πΆβπ))) β§ π΄ β π΅) β π β 0) | ||
Theorem | ax5seglem5 28191* | Lemma for ax5seg 28196. If π΅ is between π΄ and πΆ, and π΄ is distinct from π΅, then π΄ is distinct from πΆ. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π΄ β π΅ β§ π β (0[,]1) β§ βπ β (1...π)(π΅βπ) = (((1 β π) Β· (π΄βπ)) + (π Β· (πΆβπ))))) β Ξ£π β (1...π)(((π΄βπ) β (πΆβπ))β2) β 0) | ||
Theorem | ax5seglem6 28192* | Lemma for ax5seg 28196. Given two line segments that are divided into pieces, if the pieces are congruent, then the scaling constant is the same. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ (((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ)))) β§ (π΄ β π΅ β§ (π β (0[,]1) β§ π β (0[,]1)) β§ (βπ β (1...π)(π΅βπ) = (((1 β π) Β· (π΄βπ)) + (π Β· (πΆβπ))) β§ βπ β (1...π)(πΈβπ) = (((1 β π) Β· (π·βπ)) + (π Β· (πΉβπ))))) β§ (β¨π΄, π΅β©Cgrβ¨π·, πΈβ© β§ β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©)) β π = π) | ||
Theorem | ax5seglem7 28193 | Lemma for ax5seg 28196. An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ π΄ β β & β’ π β β & β’ πΆ β β & β’ π· β β β β’ (π Β· ((πΆ β π·)β2)) = ((((((1 β π) Β· π΄) + (π Β· πΆ)) β π·)β2) + ((1 β π) Β· ((π Β· ((π΄ β πΆ)β2)) β ((π΄ β π·)β2)))) | ||
Theorem | ax5seglem8 28194 | Lemma for ax5seg 28196. Use the weak deduction theorem to eliminate the hypotheses from ax5seglem7 28193. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ (((π΄ β β β§ π β β) β§ (πΆ β β β§ π· β β)) β (π Β· ((πΆ β π·)β2)) = ((((((1 β π) Β· π΄) + (π Β· πΆ)) β π·)β2) + ((1 β π) Β· ((π Β· ((π΄ β πΆ)β2)) β ((π΄ β π·)β2))))) | ||
Theorem | ax5seglem9 28195* | Lemma for ax5seg 28196. Take the calculation in ax5seglem8 28194 and turn it into a series of measurements. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.) |
β’ (((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)))) β§ (π β (0[,]1) β§ βπ β (1...π)(π΅βπ) = (((1 β π) Β· (π΄βπ)) + (π Β· (πΆβπ))))) β (π Β· Ξ£π β (1...π)(((πΆβπ) β (π·βπ))β2)) = (Ξ£π β (1...π)(((π΅βπ) β (π·βπ))β2) + ((1 β π) Β· ((π Β· Ξ£π β (1...π)(((π΄βπ) β (πΆβπ))β2)) β Ξ£π β (1...π)(((π΄βπ) β (π·βπ))β2))))) | ||
Theorem | ax5seg 28196 | The five segment axiom. Take two triangles π΄π·πΆ and πΈπ»πΊ, a point π΅ on π΄πΆ, and a point πΉ on πΈπΊ. If all corresponding line segments except for πΆπ· and πΊπ» are congruent, then so are πΆπ· and πΊπ». Axiom A5 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (((π΄ β π΅ β§ π΅ Btwn β¨π΄, πΆβ© β§ πΉ Btwn β¨πΈ, πΊβ©) β§ (β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ© β§ β¨π΅, πΆβ©Cgrβ¨πΉ, πΊβ©) β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨π΅, π·β©Cgrβ¨πΉ, π»β©)) β β¨πΆ, π·β©Cgrβ¨πΊ, π»β©)) | ||
Theorem | axbtwnid 28197 | Points are indivisible. That is, if π΄ lies between π΅ and π΅, then π΄ = π΅. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (π΄ Btwn β¨π΅, π΅β© β π΄ = π΅)) | ||
Theorem | axpaschlem 28198* | Lemma for axpasch 28199. Set up coefficents used in the proof. (Contributed by Scott Fenton, 5-Jun-2013.) |
β’ ((π β (0[,]1) β§ π β (0[,]1)) β βπ β (0[,]1)βπ β (0[,]1)(π = ((1 β π) Β· (1 β π)) β§ π = ((1 β π) Β· (1 β π)) β§ ((1 β π) Β· π) = ((1 β π) Β· π))) | ||
Theorem | axpasch 28199* | The inner Pasch axiom. Take a triangle π΄πΆπΈ, a point π· on π΄πΆ, and a point π΅ extending πΆπΈ. Then π΄πΈ and π·π΅ intersect at some point π₯. Axiom A7 of [Schwabhauser] p. 12. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ))) β ((π· Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π΅, πΆβ©) β βπ₯ β (πΌβπ)(π₯ Btwn β¨π·, π΅β© β§ π₯ Btwn β¨πΈ, π΄β©))) | ||
Theorem | axlowdimlem1 28200 | Lemma for axlowdim 28219. Establish a particular constant function as a function. (Contributed by Scott Fenton, 29-Jun-2013.) |
β’ ((3...π) Γ {0}):(3...π)βΆβ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |