![]() |
Metamath
Proof Explorer Theorem List (p. 282 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cgrane1 28101 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | cgrane2 28102 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΅ β πΆ) | ||
Theorem | cgrane3 28103 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β π·) | ||
Theorem | cgrane4 28104 | Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΈ β πΉ) | ||
Theorem | cgrahl1 28105 | 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 28106 | 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 28107 | 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 28108 | 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 28109 | 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 28110 | 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 28111 | 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 28112 | 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 28113 | Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΉ)) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π· β πΈ) & β’ (π β πΉ β πΈ) β β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) | ||
Theorem | cgraswaplr 28114 | Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) β β’ (π β β¨βπΆπ΅π΄ββ©(cgrAβπΊ)β¨βπΉπΈπ·ββ©) | ||
Theorem | cgrabtwn 28115 | 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 28116 | 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 28117 | Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | cgrancol 28118 | Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) & β’ πΏ = (LineGβπΊ) & β’ (π β Β¬ (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) β β’ (π β Β¬ (πΉ β (π·πΏπΈ) β¨ π· = πΈ)) | ||
Theorem | dfcgra2 28119* | 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 28097 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β ((π΄ β π΅ β§ πΆ β π΅) β§ (π· β πΈ β§ πΉ β πΈ) β§ βπ β π βπ β π βπ β π βπ β π (((π΄ β (π΅πΌπ) β§ (π΄ β π) = (πΈ β π·)) β§ (πΆ β (π΅πΌπ) β§ (πΆ β π) = (πΈ β πΉ))) β§ ((π· β (πΈπΌπ) β§ (π· β π) = (π΅ β π΄)) β§ (πΉ β (πΈπΌπ) β§ (πΉ β π) = (π΅ β πΆ))) β§ (π β π) = (π β π))))) | ||
Theorem | sacgr 28120 | 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 28121 | 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 28122* | 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 28123 | 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 28124 | Extend class relation with the geometrical "point in angle" relation. |
class inA | ||
Syntax | cleag 28125 | Extend class relation with the "angle less than" relation. |
class β€β | ||
Definition | df-inag 28126* | 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 28127* | 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 28128 | Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π β (π΄πΌπΆ)) & β’ (π β (π = π΅ β¨ π(πΎβπ΅)π)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagflat 28129 | Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) | ||
Theorem | inagswap 28130 | 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 28131 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π΄ β π΅) | ||
Theorem | inagne2 28132 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β πΆ β π΅) | ||
Theorem | inagne3 28133 | Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΎ = (hlGβπΊ) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β πΊ β TarskiG) & β’ (π β π(inAβπΊ)β¨βπ΄π΅πΆββ©) β β’ (π β π β π΅) | ||
Theorem | inaghl 28134 | 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 28135* | 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 28136* | 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 28137 | Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ β€ = (β€β βπΊ) & β’ (π β π β π) & β’ (π β π(inAβπΊ)β¨βπ·πΈπΉββ©) & β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπββ©) β β’ (π β β¨βπ΄π΅πΆββ© β€ β¨βπ·πΈπΉββ©) | ||
Theorem | leagne1 28138 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π΄ β π΅) | ||
Theorem | leagne2 28139 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΆ β π΅) | ||
Theorem | leagne3 28140 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β π· β πΈ) | ||
Theorem | leagne4 28141 | Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ©(β€β βπΊ)β¨βπ·πΈπΉββ©) β β’ (π β πΉ β πΈ) | ||
Theorem | cgrg3col4 28142* | 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 28143 | 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 28144 | 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 28145 | 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 28146 | 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 28147 | 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 28148 | 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 28149 | 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 28150 | 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 28151 | 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 28152 | 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 27800, already covers that part: see trgcgr 27805. 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 27805. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) β β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β (((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)) β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)))) | ||
Theorem | isoas 28153 | 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 28154 | Declare the class of equilateral triangles. |
class eqltrG | ||
Definition | df-eqlg 28155* | 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 28156 | Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β (β¨βπ΄π΅πΆββ© β (eqltrGβπΊ) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ΅πΆπ΄ββ©)) | ||
Theorem | iseqlgd 28157 | Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ πΏ = (LineGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π΄ β π΅) = (π΅ β πΆ)) & β’ (π β (π΅ β πΆ) = (πΆ β π΄)) & β’ (π β (πΆ β π΄) = (π΄ β π΅)) β β’ (π β β¨βπ΄π΅πΆββ© β (eqltrGβπΊ)) | ||
Theorem | f1otrgds 28158* | Convenient lemma for f1otrg 28160. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) | ||
Theorem | f1otrgitv 28159* | Convenient lemma for f1otrg 28160. (Contributed by Thierry Arnoux, 19-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ π· = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ π΅ = (Baseβπ») & β’ πΈ = (distβπ») & β’ π½ = (Itvβπ») & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΈπ) = ((πΉβπ)π·(πΉβπ))) & β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) | ||
Theorem | f1otrg 28160* | 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 28161* | 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 28162 | Function to convert an algebraic structure to a Tarski geometry. |
class toTG | ||
Definition | df-ttg 28163* | 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 28164* | 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 28165* | Obsolete proof of ttgval 28164 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 28166 | Lemma for ttgbas 28168, ttgvsca 28173 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 28167 | Obsolete version of ttglem 28166 as of 29-Oct-2024. Lemma for ttgbas 28168 and ttgvsca 28173. (Contributed by Thierry Arnoux, 15-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (toTGβπ») & β’ πΈ = Slot π & β’ π β β & β’ π < ;16 β β’ (πΈβπ») = (πΈβπΊ) | ||
Theorem | ttgbas 28168 | 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 28169 | Obsolete proof of ttgbas 28168 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 28170 | 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 28171 | Obsolete proof of ttgplusg 28170 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 28172 | The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ β = (-gβπ») β β’ β = (-gβπΊ) | ||
Theorem | ttgvsca 28173 | 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 28174 | Obsolete proof of ttgvsca 28173 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 28175 | 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 28176 | Obsolete proof of ttgds 28175 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 28177* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») β β’ ((π» β π β§ π β π β§ π β π) β (ππΌπ) = {π§ β π β£ βπ β (0[,]1)(π§ β π) = (π Β· (π β π))}) | ||
Theorem | ttgelitv 28178* | Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) |
β’ πΊ = (toTGβπ») & β’ πΌ = (ItvβπΊ) & β’ π = (Baseβπ») & β’ β = (-gβπ») & β’ Β· = ( Β·π βπ») & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π» β π) & β’ (π β π β π) β β’ (π β (π β (ππΌπ) β βπ β (0[,]1)(π β π) = (π Β· (π β π)))) | ||
Theorem | ttgbtwnid 28179 | 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 28180 | 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 28181 | Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.) |
β’ (πΊ β βMetSp β πΊ β TarskiGC) | ||
Theorem | cchhllem 28182* | 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 28183* | Obsolete version of cchhllem 28182 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 28184 | Declare the syntax for the Euclidean space generator. |
class πΌ | ||
Syntax | cbtwn 28185 | Declare the syntax for the Euclidean betweenness predicate. |
class Btwn | ||
Syntax | ccgr 28186 | Declare the syntax for the Euclidean congruence predicate. |
class Cgr | ||
Definition | df-ee 28187 | Define the Euclidean space generator. For details, see elee 28190. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ πΌ = (π β β β¦ (β βm (1...π))) | ||
Definition | df-btwn 28188* | Define the Euclidean betweenness predicate. For details, see brbtwn 28195. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ Btwn = β‘{β¨β¨π₯, π§β©, π¦β© β£ βπ β β ((π₯ β (πΌβπ) β§ π§ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ βπ‘ β (0[,]1)βπ β (1...π)(π¦βπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π§βπ))))} | ||
Definition | df-cgr 28189* | Define the Euclidean congruence predicate. For details, see brcgr 28196. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ Cgr = {β¨π₯, π¦β© β£ βπ β β ((π₯ β ((πΌβπ) Γ (πΌβπ)) β§ π¦ β ((πΌβπ) Γ (πΌβπ))) β§ Ξ£π β (1...π)((((1st βπ₯)βπ) β ((2nd βπ₯)βπ))β2) = Ξ£π β (1...π)((((1st βπ¦)βπ) β ((2nd βπ¦)βπ))β2))} | ||
Theorem | elee 28190 | 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 28191* | A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.) |
β’ (π β β β ((π β (1...π) β¦ (π΄πΉπ΅)) β (πΌβπ) β βπ β (1...π)(π΄πΉπ΅) β β)) | ||
Theorem | eleenn 28192 | If π΄ is in (πΌβπ), then π is a natural. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ (π΄ β (πΌβπ) β π β β) | ||
Theorem | eleei 28193 | The forward direction of elee 28190. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ (π΄ β (πΌβπ) β π΄:(1...π)βΆβ) | ||
Theorem | eedimeq 28194 | A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΄ β (πΌβπ)) β π = π) | ||
Theorem | brbtwn 28195* | 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 28196* | 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 28197 | The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ πΌ β (1...π)) β (π΄βπΌ) β β) | ||
Theorem | fveecn 28198 | The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ πΌ β (1...π)) β (π΄βπΌ) β β) | ||
Theorem | eqeefv 28199* | Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (π΄ = π΅ β βπ β (1...π)(π΄βπ) = (π΅βπ))) | ||
Theorem | eqeelen 28200* | 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |