Home | Metamath
Proof Explorer Theorem List (p. 264 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | trgcgrg 26301 | The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉 ↔ ((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)))) | ||
Theorem | trgcgr 26302 | Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) | ||
Theorem | ercgrg 26303 | 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 26304* | 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 26305 | Reflexivity law for three-place congruence. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐴𝐵𝐶”〉) | ||
Theorem | cgr3simp1 26306 | 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 26307 | 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 26308 | 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 26309 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐵𝐴𝐶”〉 ∼ 〈“𝐸𝐷𝐹”〉) | ||
Theorem | cgr3swap23 26310 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐶𝐵”〉 ∼ 〈“𝐷𝐹𝐸”〉) | ||
Theorem | cgr3swap13 26311 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 3-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉 ∼ 〈“𝐹𝐸𝐷”〉) | ||
Theorem | cgr3rotr 26312 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉 ∼ 〈“𝐹𝐷𝐸”〉) | ||
Theorem | cgr3rotl 26313 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐵𝐶𝐴”〉 ∼ 〈“𝐸𝐹𝐷”〉) | ||
Theorem | trgcgrcom 26314 | Commutative law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∼ 〈“𝐴𝐵𝐶”〉) | ||
Theorem | cgr3tr 26315 | Transitivity law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐾 ∈ 𝑃) & ⊢ (𝜑 → 𝐿 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∼ 〈“𝐽𝐾𝐿”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐽𝐾𝐿”〉) | ||
Theorem | tgbtwnxfr 26316 | 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 26317 | 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 26318 | Declare the constant for the isometry builder. |
class Ismt | ||
Definition | df-ismt 26319* | Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 26320. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
⊢ Ismt = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))}) | ||
Theorem | isismt 26320* | Property of being an isometry. Compare with isismty 35094. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ − = (dist‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) | ||
Theorem | ismot 26321* | 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 26322 | Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | idmot 26323 | The identity is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( I ↾ 𝑃) ∈ (𝐺Ismt𝐺)) | ||
Theorem | motf1o 26324 | Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → 𝐹:𝑃–1-1-onto→𝑃) | ||
Theorem | motcl 26325 | Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑃) | ||
Theorem | motco 26326 | The composition of two motions is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐺Ismt𝐺)) | ||
Theorem | cnvmot 26327 | The converse of a motion is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → ◡𝐹 ∈ (𝐺Ismt𝐺)) | ||
Theorem | motplusg 26328* | 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 26329* | 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 26330* | 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 26331 | 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 26332* | 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 26333 | Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → 𝐿 Fn ((𝑃 × 𝑃) ∖ I )) | ||
Theorem | tglnunirn 26334 | Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃) | ||
Theorem | tglnpt 26335 | Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑃) | ||
Theorem | tglngne 26336 | It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
Theorem | tglngval 26337* | The line going through points 𝑋 and 𝑌. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) ⇒ ⊢ (𝜑 → (𝑋𝐿𝑌) = {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))}) | ||
Theorem | tglnssp 26338 | 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 26339 | 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 26340 | 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 26341 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
Theorem | btwncolg2 26342 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
Theorem | btwncolg3 26343 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
Theorem | colcom 26344 | 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 26345 | 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 26346 | 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 26347 | Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋)) | ||
Theorem | ncolrot1 26348 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) | ||
Theorem | ncolrot2 26349 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑌 ∈ (𝑍𝐿𝑋) ∨ 𝑍 = 𝑋)) | ||
Theorem | tgdim01ln 26350 | 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 26351 | If there are three non-colinear points, then the dimension is at least two. Converse of tglowdim2l 26436. (Contributed by Thierry Arnoux, 23-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → 𝐺DimTarskiG≥2) | ||
Theorem | lnxfr 26352 | 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 26353* | 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 26354 | 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 26355 | 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 26356 | 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 26357 | 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 26358 | Lemma for tgbtwnconn1 26361. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) ⇒ ⊢ (𝜑 → 𝐻 = 𝐽) | ||
Theorem | tgbtwnconn1lem2 26359 | Lemma for tgbtwnconn1 26361. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 − 𝐹) = (𝐶 − 𝐷)) | ||
Theorem | tgbtwnconn1lem3 26360 | Lemma for tgbtwnconn1 26361. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐼𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → 𝐶 ≠ 𝐸) ⇒ ⊢ (𝜑 → 𝐷 = 𝐹) | ||
Theorem | tgbtwnconn1 26361 | 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 26362 | Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))) | ||
Theorem | tgbtwnconn3 26363 | Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) | ||
Theorem | tgbtwnconnln3 26364 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) & ⊢ 𝐿 = (LineG‘𝐺) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) | ||
Theorem | tgbtwnconn22 26365 | Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐸)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐷𝐼𝐸)) | ||
Theorem | tgbtwnconnln1 26366 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
Theorem | tgbtwnconnln2 26367 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
Syntax | cleg 26368 | Less-than relation for geometric congruences. |
class ≤G | ||
Definition | df-leg 26369* | Define the less-than relationship between geometric distance congruence classes. See legval 26370. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ ≤G = (𝑔 ∈ V ↦ {〈𝑒, 𝑓〉 ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))}) | ||
Theorem | legval 26370* | Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ≤ = {〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))}) | ||
Theorem | legov 26371* | 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 26372* | 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 26373 | 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) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐵)) | ||
Theorem | btwnleg 26374 | Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐶)) | ||
Theorem | legtrd 26375 | Transitivity of the less-than relationship. Proposition 5.8 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐸 − 𝐹)) | ||
Theorem | legtri3 26376 | Equality from the less-than relationship. Proposition 5.9 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐴 − 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) | ||
Theorem | legtrid 26377 | Trichotomy law for the less-than relationship. Proposition 5.10 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∨ (𝐶 − 𝐷) ≤ (𝐴 − 𝐵))) | ||
Theorem | leg0 26378 | Degenerated (zero-length) segments are minimal. Proposition 5.11 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐴) ≤ (𝐶 − 𝐷)) | ||
Theorem | legeq 26379 | Deduce equality from "less than" null segments. (Contributed by Thierry Arnoux, 12-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | legbtwn 26380 | Deduce betweenness from "less than" relation. Corresponds loosely to Proposition 6.13 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))) & ⊢ (𝜑 → (𝐶 − 𝐴) ≤ (𝐶 − 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐶𝐼𝐵)) | ||
Theorem | tgcgrsub2 26381 | Removing identical parts from the end of a line segment preserves congruence. In this version the order of points is not known. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) & ⊢ (𝜑 → (𝐸 ∈ (𝐷𝐼𝐹) ∨ 𝐹 ∈ (𝐷𝐼𝐸))) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) | ||
Theorem | ltgseg 26382* | The set 𝐸 denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐸 = ( − “ (𝑃 × 𝑃)) & ⊢ (𝜑 → Fun − ) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝐴 = (𝑥 − 𝑦)) | ||
Theorem | ltgov 26383 | Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐸 = ( − “ (𝑃 × 𝑃)) & ⊢ (𝜑 → Fun − ) & ⊢ < = (( ≤ ↾ 𝐸) ∖ I ) & ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − ) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷)))) | ||
Theorem | legov3 26384 | An equivalent definition of the less-than relationship, from the strict relation. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐸 = ( − “ (𝑃 × 𝑃)) & ⊢ (𝜑 → Fun − ) & ⊢ < = (( ≤ ↾ 𝐸) ∖ I ) & ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − ) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) < (𝐶 − 𝐷) ∨ (𝐴 − 𝐵) = (𝐶 − 𝐷)))) | ||
Theorem | legso 26385 | The "shorter than" relation induces an order on pairs. Remark 5.13 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐸 = ( − “ (𝑃 × 𝑃)) & ⊢ (𝜑 → Fun − ) & ⊢ < = (( ≤ ↾ 𝐸) ∖ I ) & ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − ) ⇒ ⊢ (𝜑 → < Or 𝐸) | ||
Syntax | chlg 26386 | Function producing the relation "belong to the same half-line". |
class hlG | ||
Definition | df-hlg 26387* | Define the function producting the relation "belong to the same half-line" (Contributed by Thierry Arnoux, 15-Aug-2020.) |
⊢ hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))})) | ||
Theorem | ishlg 26388 | Rays : Definition 6.1 of [Schwabhauser] p. 43. With this definition, 𝐴(𝐾‘𝐶)𝐵 means that 𝐴 and 𝐵 are on the same ray with initial point 𝐶. This follows the same notation as Schwabhauser where rays are first defined as a relation. It is possible to recover the ray itself using e.g. ((𝐾‘𝐶) “ {𝐴}) (Contributed by Thierry Arnoux, 21-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))) | ||
Theorem | hlcomb 26389 | The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐵(𝐾‘𝐶)𝐴)) | ||
Theorem | hlcomd 26390 | The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐵(𝐾‘𝐶)𝐴) | ||
Theorem | hlne1 26391 | The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | hlne2 26392 | The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | hlln 26393 | The half-line relation implies colinearity, part of Theorem 6.4 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶)) | ||
Theorem | hleqnid 26394 | The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝐵) | ||
Theorem | hlid 26395 | The half-line relation is reflexive. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐴) | ||
Theorem | hltr 26396 | The half-line relation is transitive. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 23-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵) & ⊢ (𝜑 → 𝐵(𝐾‘𝐷)𝐶) ⇒ ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐶) | ||
Theorem | hlbtwn 26397 | Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐶𝐼𝐵)) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐷 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐴(𝐾‘𝐶)𝐷)) | ||
Theorem | btwnhl1 26398 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → 𝐶(𝐾‘𝐴)𝐵) | ||
Theorem | btwnhl2 26399 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐴) | ||
Theorem | btwnhl 26400 | Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐼𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |