![]() |
Metamath
Proof Explorer Theorem List (p. 287 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cgratr 28601 | 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 28602 | Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΉ)) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π· β πΈ) & β’ (π β πΉ β πΈ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgraswaplr 28603 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β β¨βπΆπ΅π΄ββ©(cgrAβπΊ)β¨βπΉπΈπ·ββ©) | ||
Theorem | cgrabtwn 28604 | 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 28605 | 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 28606 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | cgrancol 28607 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β Β¬ (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | dfcgra2 28608* | 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 28586 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β ((π΄ β π΅ β§ πΆ β π΅) β§ (π· β πΈ β§ πΉ β πΈ) β§ βπ β π βπ β π βπ β π βπ β π (((π΄ β (π΅πΌπ) β§ (π΄ β π) = (πΈ β π·)) β§ (πΆ β (π΅πΌπ) β§ (πΆ β π) = (πΈ β πΉ))) β§ ((π· β (πΈπΌπ) β§ (π· β π) = (π΅ β π΄)) β§ (πΉ β (πΈπΌπ) β§ (πΉ β π) = (π΅ β πΆ))) β§ (π β π) = (π β π))))) | ||
Theorem | sacgr 28609 | 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 28610 | 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 28611* | 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 28612 | 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 28613 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 28614 | Extend class relation with the "angle less than" relation. |
class β€β | ||
Definition | df-inag 28615* | 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 28616* | 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 28617 | Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π β (π΄πΌπΆ)) & β’ (π β (π = π΅ β¨ π(πΎβπ΅)π)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagflat 28618 | Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagswap 28619 | 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 28620 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π΄ β π΅) | ||
Theorem | inagne2 28621 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β πΆ β π΅) | ||
Theorem | inagne3 28622 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π β π΅) | ||
Theorem | inaghl 28623 | 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 28624* | 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 28625* | 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 28626 | Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ β€ = (β€β βπΊ) & β’ (π β π β π) & β’ (π β π(inAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) β β’ (π β β¨βπ΄π΅πΆββ© β€ β¨βπ·πΈπΉββ©) | ||
Theorem | leagne1 28627 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | leagne2 28628 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΆ β π΅) | ||
Theorem | leagne3 28629 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π· β πΈ) | ||
Theorem | leagne4 28630 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΉ β πΈ) | ||
Theorem | cgrg3col4 28631* | 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 28632 | 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 28633 | 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 28634 | 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 28635 | 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 28636 | 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 28637 | 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 28638 | 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 28639 | 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 28640 | 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 28641 | 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 28289, already covers that part: see trgcgr 28294. 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 28294. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β (((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)) β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)))) | ||
Theorem | isoas 28642 | 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 28643 | Declare the class of equilateral triangles. |
class eqltrG | ||
Definition | df-eqlg 28644* | 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 28645 | Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β (β¨βπ΄π΅πΆββ© β (eqltrGβπΊ) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ΅πΆπ΄ββ©)) | ||
Theorem | iseqlgd 28646 | Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π΄ β π΅) = (π΅ β πΆ)) & β’ (π β (π΅ β πΆ) = (πΆ β π΄)) & β’ (π β (πΆ β π΄) = (π΄ β π΅)) β β’ (π β β¨βπ΄π΅πΆββ© β (eqltrGβπΊ)) | ||
Theorem | f1otrgds 28647* | Convenient lemma for f1otrg 28649. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) | ||
Theorem | f1otrgitv 28648* | Convenient lemma for f1otrg 28649. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) | ||
Theorem | f1otrg 28649* | 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 28650* | 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 28651 | Function to convert an algebraic structure to a Tarski geometry. |
class toTG | ||
Definition | df-ttg 28652* | 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 28653* | 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 28654* | Obsolete proof of ttgval 28653 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 28655 | Lemma for ttgbas 28657, ttgvsca 28662 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 28656 | Obsolete version of ttglem 28655 as of 29-Oct-2024. Lemma for ttgbas 28657 and ttgvsca 28662. (Contributed by Thierry Arnoux, 15-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ πΈ = Slot π & β’ π β β & β’ π < ;16 β β’ (πΈβπ») = (πΈβπΊ) | ||
Theorem | ttgbas 28657 | 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 28658 | Obsolete proof of ttgbas 28657 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 28659 | 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 28660 | Obsolete proof of ttgplusg 28659 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 28661 | The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ β = (-gβπ») β β’ β = (-gβπΊ) | ||
Theorem | ttgvsca 28662 | 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 28663 | Obsolete proof of ttgvsca 28662 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 28664 | 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 28665 | Obsolete proof of ttgds 28664 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 28666* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») β β’ ((π» β π β§ π β π β§ π β π) β (ππΌπ) = {π§ β π β£ βπ β (0[,]1)(π§ β π) = (π Β· (π β π))}) | ||
Theorem | ttgelitv 28667* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π» β π) & β’ (π β π β π) β β’ (π β (π β (ππΌπ) β βπ β (0[,]1)(π β π) = (π Β· (π β π)))) | ||
Theorem | ttgbtwnid 28668 | 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 28669 | 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 28670 | Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.) |
β’ (πΊ β βMetSp β πΊ β TarskiGC) | ||
Theorem | cchhllem 28671* | 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 28672* | Obsolete version of cchhllem 28671 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 28673 | Declare the syntax for the Euclidean space generator. |
class πΌ | ||
Syntax | cbtwn 28674 | Declare the syntax for the Euclidean betweenness predicate. |
class Btwn | ||
Syntax | ccgr 28675 | Declare the syntax for the Euclidean congruence predicate. |
class Cgr | ||
Definition | df-ee 28676 | Define the Euclidean space generator. For details, see elee 28679. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ πΌ = (π β β β¦ (β βm (1...π))) | ||
Definition | df-btwn 28677* | Define the Euclidean betweenness predicate. For details, see brbtwn 28684. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ Btwn = β‘{β¨β¨π₯, π§β©, π¦β© β£ βπ β β ((π₯ β (πΌβπ) β§ π§ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ βπ‘ β (0[,]1)βπ β (1...π)(π¦βπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π§βπ))))} | ||
Definition | df-cgr 28678* | Define the Euclidean congruence predicate. For details, see brcgr 28685. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ Cgr = {β¨π₯, π¦β© β£ βπ β β ((π₯ β ((πΌβπ) Γ (πΌβπ)) β§ π¦ β ((πΌβπ) Γ (πΌβπ))) β§ Ξ£π β (1...π)((((1st βπ₯)βπ) β ((2nd βπ₯)βπ))β2) = Ξ£π β (1...π)((((1st βπ¦)βπ) β ((2nd βπ¦)βπ))β2))} | ||
Theorem | elee 28679 | 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 28680* | A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.) |
β’ (π β β β ((π β (1...π) β¦ (π΄πΉπ΅)) β (πΌβπ) β βπ β (1...π)(π΄πΉπ΅) β β)) | ||
Theorem | eleenn 28681 | If π΄ is in (πΌβπ), then π is a natural. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ (π΄ β (πΌβπ) β π β β) | ||
Theorem | eleei 28682 | The forward direction of elee 28679. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ (π΄ β (πΌβπ) β π΄:(1...π)βΆβ) | ||
Theorem | eedimeq 28683 | A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΄ β (πΌβπ)) β π = π) | ||
Theorem | brbtwn 28684* | 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 28685* | 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 28686 | The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ πΌ β (1...π)) β (π΄βπΌ) β β) | ||
Theorem | fveecn 28687 | The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ πΌ β (1...π)) β (π΄βπΌ) β β) | ||
Theorem | eqeefv 28688* | Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (π΄ = π΅ β βπ β (1...π)(π΄βπ) = (π΅βπ))) | ||
Theorem | eqeelen 28689* | 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 28690* | Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β (π΄ Btwn β¨π΅, πΆβ© β (βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) β€ 0 β§ βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ)))))) | ||
Theorem | colinearalglem1 28691 | Lemma for colinearalg 28695. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π· β β β§ πΈ β β β§ πΉ β β)) β (((π΅ β π΄) Β· (πΉ β π·)) = ((πΈ β π·) Β· (πΆ β π΄)) β ((π΅ Β· πΉ) β ((π΄ Β· πΉ) + (π΅ Β· π·))) = ((πΆ Β· πΈ) β ((π΄ Β· πΈ) + (πΆ Β· π·))))) | ||
Theorem | colinearalglem2 28692* | Lemma for colinearalg 28695. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β (βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) β βπ β (1...π)βπ β (1...π)(((πΆβπ) β (π΅βπ)) Β· ((π΄βπ) β (π΅βπ))) = (((πΆβπ) β (π΅βπ)) Β· ((π΄βπ) β (π΅βπ))))) | ||
Theorem | colinearalglem3 28693* | Lemma for colinearalg 28695. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β (βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) β βπ β (1...π)βπ β (1...π)(((π΄βπ) β (πΆβπ)) Β· ((π΅βπ) β (πΆβπ))) = (((π΄βπ) β (πΆβπ)) Β· ((π΅βπ) β (πΆβπ))))) | ||
Theorem | colinearalglem4 28694* | Lemma for colinearalg 28695. 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 28695* | An algebraic characterization of colinearity. Note the similarity to brbtwn2 28690. (Contributed by Scott Fenton, 24-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β ((π΄ Btwn β¨π΅, πΆβ© β¨ π΅ Btwn β¨πΆ, π΄β© β¨ πΆ Btwn β¨π΄, π΅β©) β βπ β (1...π)βπ β (1...π)(((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))) = (((π΅βπ) β (π΄βπ)) Β· ((πΆβπ) β (π΄βπ))))) | ||
Theorem | eleesub 28696* | Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.) |
β’ πΆ = (π β (1...π) β¦ ((π΄βπ) β (π΅βπ))) β β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β πΆ β (πΌβπ)) | ||
Theorem | eleesubd 28697* | Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 28696. (Contributed by Scott Fenton, 17-Jul-2013.) |
β’ (π β πΆ = (π β (1...π) β¦ ((π΄βπ) β (π΅βπ)))) β β’ ((π β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β πΆ β (πΌβπ)) | ||
Theorem | axdimuniq 28698 | 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 28699 | π΄ is as far from π΅ as π΅ is from π΄. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΅β©Cgrβ¨π΅, π΄β©) | ||
Theorem | axcgrtr 28700 | Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |