Home | Metamath
Proof Explorer Theorem List (p. 263 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tgbtwncom 26201 | Betweenness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴)) | ||
Theorem | tgbtwncomb 26202 | Betweenness commutes, biconditional version. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ↔ 𝐵 ∈ (𝐶𝐼𝐴))) | ||
Theorem | tgbtwnne 26203 | Betweenness and inequality. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ≠ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | tgbtwntriv1 26204 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐼𝐵)) | ||
Theorem | tgbtwnswapid 26205 | If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | tgbtwnintr 26206 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐷)) & ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) | ||
Theorem | tgbtwnexch3 26207 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) | ||
Theorem | tgbtwnouttr2 26208 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgbtwnexch2 26209 | Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgbtwnouttr 26210 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgbtwnexch 26211 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) | ||
Theorem | tgtrisegint 26212* | A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of [Schwabhauser] p. 33. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐶)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝐹𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸))) | ||
Theorem | tglowdim1 26213* | Lower dimension axiom for one dimension. In dimension at least 1, there are at least two distinct points. The condition "the space is of dimension 1 or more" is written here as 2 ≤ (♯‘𝑃) to avoid a new definition, but a different convention could be chosen. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝑥 ≠ 𝑦) | ||
Theorem | tglowdim1i 26214* | Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝑃 𝑋 ≠ 𝑦) | ||
Theorem | tgldimor 26215 | Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
⊢ 𝑃 = (𝐸‘𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤ (♯‘𝑃))) | ||
Theorem | tgldim0eq 26216 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
⊢ 𝑃 = (𝐸‘𝐹) & ⊢ (𝜑 → (♯‘𝑃) = 1) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | tgldim0itv 26217 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (♯‘𝑃) = 1) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶)) | ||
Theorem | tgldim0cgr 26218 | In dimension zero, any two pairs of points are congruent. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (♯‘𝑃) = 1) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) | ||
Theorem | tgbtwndiff 26219* | There is always a 𝑐 distinct from 𝐵 such that 𝐵 lies between 𝐴 and 𝑐. Theorem 3.14 of [Schwabhauser] p. 32. The condition "the space is of dimension 1 or more" is written here as 2 ≤ (♯‘𝑃) for simplicity. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑐) ∧ 𝐵 ≠ 𝑐)) | ||
Theorem | tgdim01 26220 | In geometries of dimension less than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) | ||
Theorem | tgifscgr 26221 | Inner five segment congruence. Take two triangles, 𝐴𝐷𝐶 and 𝐸𝐻𝐾, with 𝐵 between 𝐴 and 𝐶 and 𝐹 between 𝐸 and 𝐾. If the other components of the triangles are congruent, then so are 𝐵𝐷 and 𝐹𝐻. Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐾 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐹 ∈ (𝐸𝐼𝐾)) & ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐸 − 𝐾)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐹 − 𝐾)) & ⊢ (𝜑 → (𝐴 − 𝐷) = (𝐸 − 𝐻)) & ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐾 − 𝐻)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐷) = (𝐹 − 𝐻)) | ||
Theorem | tgcgrsub 26222 | Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | ||
Syntax | ccgrg 26223 | Declare the constant for the congruence between shapes relation. |
class cgrG | ||
Definition | df-cgrg 26224* |
Define the relation of congruence between shapes. Definition 4.4 of
[Schwabhauser] p. 35. A
"shape" is a finite sequence of points, and a
triangle can be represented as a shape with three points. Two shapes
are congruent if all corresponding segments between all corresponding
points are congruent.
Many systems of geometry define triangle congruence as requiring both segment congruence and angle congruence. Such systems, such as Hilbert's axiomatic system, typically have a primitive notion of angle congruence in addition to segment congruence. Here, angle congruence is instead a derived notion, defined later in df-cgra 26521 and expanded in iscgra 26522. This does not mean our system is weaker; dfcgrg2 26576 proves that these two definitions are equivalent, and using the Tarski definition instead (given in [Schwabhauser] p. 35) is simpler. Once two triangles are proven congruent as defined here, you can use various theorems to prove that corresponding parts of congruent triangles are congruent (CPCTC). For example, see cgr3simp1 26233, cgr3simp2 26234, cgr3simp3 26235, cgrcgra 26534, and permutation laws such as cgr3swap12 26236 and dfcgrg2 26576. Ideally, we would define this for functions of any set, but we will use words (see df-word 13850) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ cgrG = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}) | ||
Theorem | iscgrg 26225* | The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))) | ||
Theorem | iscgrgd 26226* | The property for two sequences 𝐴 and 𝐵 of points to be congruent. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐴:𝐷⟶𝑃) & ⊢ (𝜑 → 𝐵:𝐷⟶𝑃) ⇒ ⊢ (𝜑 → (𝐴 ∼ 𝐵 ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) | ||
Theorem | iscgrglt 26227* | The property for two sequences 𝐴 and 𝐵 of points to be congruent, where the congruence is only required for indices verifying a less-than relation. (Contributed by Thierry Arnoux, 7-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐴:𝐷⟶𝑃) & ⊢ (𝜑 → 𝐵:𝐷⟶𝑃) ⇒ ⊢ (𝜑 → (𝐴 ∼ 𝐵 ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴(𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) | ||
Theorem | trgcgrg 26228 | The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉 ↔ ((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)))) | ||
Theorem | trgcgr 26229 | Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) | ||
Theorem | ercgrg 26230 | The shape congruence relation is an equivalence relation. Statement 4.4 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → (cgrG‘𝐺) Er (𝑃 ↑pm ℝ)) | ||
Theorem | tgcgrxfr 26231* | A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝑒𝐹”〉)) | ||
Theorem | cgr3id 26232 | Reflexivity law for three-place congruence. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐴𝐵𝐶”〉) | ||
Theorem | cgr3simp1 26233 | Deduce segment congruence from a triangle congruence. This is a portion of the theorem that corresponding parts of congruent triangles are congruent (CPCTC), focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | ||
Theorem | cgr3simp2 26234 | Deduce segment congruence from a triangle congruence. This is a portion of CPCTC, focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) | ||
Theorem | cgr3simp3 26235 | Deduce segment congruence from a triangle congruence. This is a portion of CPCTC, focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) | ||
Theorem | cgr3swap12 26236 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐵𝐴𝐶”〉 ∼ 〈“𝐸𝐷𝐹”〉) | ||
Theorem | cgr3swap23 26237 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐶𝐵”〉 ∼ 〈“𝐷𝐹𝐸”〉) | ||
Theorem | cgr3swap13 26238 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 3-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉 ∼ 〈“𝐹𝐸𝐷”〉) | ||
Theorem | cgr3rotr 26239 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉 ∼ 〈“𝐹𝐷𝐸”〉) | ||
Theorem | cgr3rotl 26240 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐵𝐶𝐴”〉 ∼ 〈“𝐸𝐹𝐷”〉) | ||
Theorem | trgcgrcom 26241 | Commutative law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∼ 〈“𝐴𝐵𝐶”〉) | ||
Theorem | cgr3tr 26242 | Transitivity law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐾 ∈ 𝑃) & ⊢ (𝜑 → 𝐿 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∼ 〈“𝐽𝐾𝐿”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐽𝐾𝐿”〉) | ||
Theorem | tgbtwnxfr 26243 | A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of [Schwabhauser] p. 36. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) | ||
Theorem | tgcgr4 26244 | Two quadrilaterals to be congruent to each other if one triangle formed by their vertices is, and the additional points are equidistant too. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶𝐷”〉 ∼ 〈“𝑊𝑋𝑌𝑍”〉 ↔ (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑊𝑋𝑌”〉 ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍))))) | ||
Syntax | cismt 26245 | Declare the constant for the isometry builder. |
class Ismt | ||
Definition | df-ismt 26246* | Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 26247. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
⊢ Ismt = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))}) | ||
Theorem | isismt 26247* | Property of being an isometry. Compare with isismty 34960. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ − = (dist‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) | ||
Theorem | ismot 26248* | Property of being an isometry mapping to the same space. In geometry, this is also called a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → (𝐹 ∈ (𝐺Ismt𝐺) ↔ (𝐹:𝑃–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎 − 𝑏)))) | ||
Theorem | motcgr 26249 | Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | idmot 26250 | The identity is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( I ↾ 𝑃) ∈ (𝐺Ismt𝐺)) | ||
Theorem | motf1o 26251 | Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → 𝐹:𝑃–1-1-onto→𝑃) | ||
Theorem | motcl 26252 | Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑃) | ||
Theorem | motco 26253 | The composition of two motions is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐺Ismt𝐺)) | ||
Theorem | cnvmot 26254 | The converse of a motion is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → ◡𝐹 ∈ (𝐺Ismt𝐺)) | ||
Theorem | motplusg 26255* | The operation for motions is their composition. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ 𝐼 = {〈(Base‘ndx), (𝐺Ismt𝐺)〉, 〈(+g‘ndx), (𝑓 ∈ (𝐺Ismt𝐺), 𝑔 ∈ (𝐺Ismt𝐺) ↦ (𝑓 ∘ 𝑔))〉} & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → (𝐹(+g‘𝐼)𝐻) = (𝐹 ∘ 𝐻)) | ||
Theorem | motgrp 26256* | The motions of a geometry form a group with respect to function composition, called the Isometry group. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ 𝐼 = {〈(Base‘ndx), (𝐺Ismt𝐺)〉, 〈(+g‘ndx), (𝑓 ∈ (𝐺Ismt𝐺), 𝑔 ∈ (𝐺Ismt𝐺) ↦ (𝑓 ∘ 𝑔))〉} ⇒ ⊢ (𝜑 → 𝐼 ∈ Grp) | ||
Theorem | motcgrg 26257* | Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ 𝐼 = {〈(Base‘ndx), (𝐺Ismt𝐺)〉, 〈(+g‘ndx), (𝑓 ∈ (𝐺Ismt𝐺), 𝑔 ∈ (𝐺Ismt𝐺) ↦ (𝑓 ∘ 𝑔))〉} & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ Word 𝑃) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝑇) ∼ 𝑇) | ||
Theorem | motcgr3 26258 | Property of a motion: distances are preserved, special case of triangles. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 = (𝐻‘𝐴)) & ⊢ (𝜑 → 𝐸 = (𝐻‘𝐵)) & ⊢ (𝜑 → 𝐹 = (𝐻‘𝐶)) & ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) | ||
Theorem | tglng 26259* | Lines of a Tarski Geometry. This relates to both Definition 4.10 of [Schwabhauser] p. 36. and Definition 6.14 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → 𝐿 = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})) | ||
Theorem | tglnfn 26260 | Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → 𝐿 Fn ((𝑃 × 𝑃) ∖ I )) | ||
Theorem | tglnunirn 26261 | Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃) | ||
Theorem | tglnpt 26262 | Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑃) | ||
Theorem | tglngne 26263 | It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
Theorem | tglngval 26264* | The line going through points 𝑋 and 𝑌. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) ⇒ ⊢ (𝜑 → (𝑋𝐿𝑌) = {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))}) | ||
Theorem | tglnssp 26265 | Lines are subset of the geometry base set. That is, lines are sets of points. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) ⇒ ⊢ (𝜑 → (𝑋𝐿𝑌) ⊆ 𝑃) | ||
Theorem | tgellng 26266 | Property of lying on the line going through points 𝑋 and 𝑌. Definition 4.10 of [Schwabhauser] p. 36. We choose the notation 𝑍 ∈ (𝑋(LineG‘𝐺)𝑌) instead of "colinear" because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))) | ||
Theorem | tgcolg 26267 | We choose the notation (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) instead of "colinear" in order to avoid defining an additional symbol for colinearity because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))) | ||
Theorem | btwncolg1 26268 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
Theorem | btwncolg2 26269 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
Theorem | btwncolg3 26270 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
Theorem | colcom 26271 | Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋)) | ||
Theorem | colrot1 26272 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) | ||
Theorem | colrot2 26273 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑍𝐿𝑋) ∨ 𝑍 = 𝑋)) | ||
Theorem | ncolcom 26274 | Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋)) | ||
Theorem | ncolrot1 26275 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) | ||
Theorem | ncolrot2 26276 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑌 ∈ (𝑍𝐿𝑋) ∨ 𝑍 = 𝑋)) | ||
Theorem | tgdim01ln 26277 | In geometries of dimension less than two, then any three points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
Theorem | ncoltgdim2 26278 | If there are three non-colinear points, then the dimension is at least two. Converse of tglowdim2l 26363. (Contributed by Thierry Arnoux, 23-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → 𝐺DimTarskiG≥2) | ||
Theorem | lnxfr 26279 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍)) & ⊢ (𝜑 → 〈“𝑋𝑌𝑍”〉 ∼ 〈“𝐴𝐵𝐶”〉) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) | ||
Theorem | lnext 26280* | Extend a line with a missing point. Theorem 4.14 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍)) & ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵)) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 〈“𝑋𝑌𝑍”〉 ∼ 〈“𝐴𝐵𝑐”〉) | ||
Theorem | tgfscgr 26281 | Congruence law for the general five segment configuration. Theorem 4.16 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍)) & ⊢ (𝜑 → 〈“𝑋𝑌𝑍”〉 ∼ 〈“𝐴𝐵𝐶”〉) & ⊢ (𝜑 → (𝑋 − 𝑇) = (𝐴 − 𝐷)) & ⊢ (𝜑 → (𝑌 − 𝑇) = (𝐵 − 𝐷)) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) ⇒ ⊢ (𝜑 → (𝑍 − 𝑇) = (𝐶 − 𝐷)) | ||
Theorem | lncgr 26282 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍)) & ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑋 − 𝐵)) & ⊢ (𝜑 → (𝑌 − 𝐴) = (𝑌 − 𝐵)) ⇒ ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − 𝐵)) | ||
Theorem | lnid 26283 | Identity law for points on lines. Theorem 4.18 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍)) & ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝐴)) & ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝐴)) ⇒ ⊢ (𝜑 → 𝑍 = 𝐴) | ||
Theorem | tgidinside 26284 | Law for finding a point inside a segment. Theorem 4.19 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝐴)) & ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝐴)) ⇒ ⊢ (𝜑 → 𝑍 = 𝐴) | ||
Theorem | tgbtwnconn1lem1 26285 | Lemma for tgbtwnconn1 26288. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) ⇒ ⊢ (𝜑 → 𝐻 = 𝐽) | ||
Theorem | tgbtwnconn1lem2 26286 | Lemma for tgbtwnconn1 26288. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 − 𝐹) = (𝐶 − 𝐷)) | ||
Theorem | tgbtwnconn1lem3 26287 | Lemma for tgbtwnconn1 26288. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐼𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → 𝐶 ≠ 𝐸) ⇒ ⊢ (𝜑 → 𝐷 = 𝐹) | ||
Theorem | tgbtwnconn1 26288 | Connectivity law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶))) | ||
Theorem | tgbtwnconn2 26289 | Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))) | ||
Theorem | tgbtwnconn3 26290 | Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) | ||
Theorem | tgbtwnconnln3 26291 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) & ⊢ 𝐿 = (LineG‘𝐺) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) | ||
Theorem | tgbtwnconn22 26292 | Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐸)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐷𝐼𝐸)) | ||
Theorem | tgbtwnconnln1 26293 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
Theorem | tgbtwnconnln2 26294 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
Syntax | cleg 26295 | Less-than relation for geometric congruences. |
class ≤G | ||
Definition | df-leg 26296* | Define the less-than relationship between geometric distance congruence classes. See legval 26297. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ ≤G = (𝑔 ∈ V ↦ {〈𝑒, 𝑓〉 ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))}) | ||
Theorem | legval 26297* | Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ≤ = {〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))}) | ||
Theorem | legov 26298* | Value of the less-than relationship. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧)))) | ||
Theorem | legov2 26299* | An equivalent definition of the less-than relationship. Definition 5.5 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷)))) | ||
Theorem | legid 26300 | Reflexivity of the less-than relationship. Proposition 5.7 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |