Home | Metamath
Proof Explorer Theorem List (p. 264 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | legid 26301 | 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 26302 | Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐶)) | ||
Theorem | legtrd 26303 | 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 26304 | 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 26305 | 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 26306 | 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 26307 | Deduce equality from "less than" null segments. (Contributed by Thierry Arnoux, 12-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | legbtwn 26308 | 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 26309 | 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 26310* | The set 𝐸 denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐸 = ( − “ (𝑃 × 𝑃)) & ⊢ (𝜑 → Fun − ) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝐴 = (𝑥 − 𝑦)) | ||
Theorem | ltgov 26311 | Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐸 = ( − “ (𝑃 × 𝑃)) & ⊢ (𝜑 → Fun − ) & ⊢ < = (( ≤ ↾ 𝐸) ∖ I ) & ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − ) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷)))) | ||
Theorem | legov3 26312 | 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 26313 | 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 26314 | Function producing the relation "belong to the same half-line". |
class hlG | ||
Definition | df-hlg 26315* | 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 26316 | 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 26317 | The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐵(𝐾‘𝐶)𝐴)) | ||
Theorem | hlcomd 26318 | The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐵(𝐾‘𝐶)𝐴) | ||
Theorem | hlne1 26319 | The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | hlne2 26320 | The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | hlln 26321 | 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 26322 | The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝐵) | ||
Theorem | hlid 26323 | 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 26324 | 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 26325 | Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐶𝐼𝐵)) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐷 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐴(𝐾‘𝐶)𝐷)) | ||
Theorem | btwnhl1 26326 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → 𝐶(𝐾‘𝐴)𝐵) | ||
Theorem | btwnhl2 26327 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐴) | ||
Theorem | btwnhl 26328 | Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐼𝐶)) | ||
Theorem | lnhl 26329 | Either a point 𝐶 on the line AB is on the same side as 𝐴 or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵)) ⇒ ⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐴 ∨ 𝐵 ∈ (𝐴𝐼𝐶))) | ||
Theorem | hlcgrex 26330* | Construct a point on a half-line, at a given distance of its origin. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐷 ≠ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥(𝐾‘𝐴)𝐷 ∧ (𝐴 − 𝑥) = (𝐵 − 𝐶))) | ||
Theorem | hlcgreulem 26331 | Lemma for hlcgreu 26332. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐷 ≠ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝐷) & ⊢ (𝜑 → 𝑌(𝐾‘𝐴)𝐷) & ⊢ (𝜑 → (𝐴 − 𝑋) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐴 − 𝑌) = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | hlcgreu 26332* | The point constructed in hlcgrex 26330 is unique. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐷 ≠ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑃 (𝑥(𝐾‘𝐴)𝐷 ∧ (𝐴 − 𝑥) = (𝐵 − 𝐶))) | ||
Theorem | btwnlng1 26333 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | btwnlng2 26334 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | btwnlng3 26335 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | lncom 26336 | 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‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ (𝑌𝐿𝑋)) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | lnrot1 26337 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐿𝑋)) & ⊢ (𝜑 → 𝑍 ≠ 𝑋) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | lnrot2 26338 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍)) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | ncolne1 26339 | Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
Theorem | ncolne2 26340 | Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) TODO (NM): maybe ncolne2 26340 could be simplified out and deleted, replaced by ncolcom 26275. |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑍) | ||
Theorem | tgisline 26341* | The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝐴 = (𝑥𝐿𝑦) ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | tglnne 26342 | It takes two different points to form a line. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
Theorem | tglndim0 26343 | There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → (♯‘𝐵) = 1) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ ran 𝐿) | ||
Theorem | tgelrnln 26344 | The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) ⇒ ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿) | ||
Theorem | tglineeltr 26345 | Transitivity law for lines, one half of tglineelsb2 26346. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ 𝑃) & ⊢ (𝜑 → 𝑆 ∈ (𝑃𝐿𝑄)) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑆)) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑄)) | ||
Theorem | tglineelsb2 26346 | If 𝑆 lies on PQ , then PQ = PS . Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ 𝑃) & ⊢ (𝜑 → 𝑆 ∈ (𝑃𝐿𝑄)) ⇒ ⊢ (𝜑 → (𝑃𝐿𝑄) = (𝑃𝐿𝑆)) | ||
Theorem | tglinerflx1 26347 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝑃𝐿𝑄)) | ||
Theorem | tglinerflx2 26348 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → 𝑄 ∈ (𝑃𝐿𝑄)) | ||
Theorem | tglinecom 26349 | Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → (𝑃𝐿𝑄) = (𝑄𝐿𝑃)) | ||
Theorem | tglinethru 26350 | If 𝐴 is a line containing two distinct points 𝑃 and 𝑄, then 𝐴 is the line through 𝑃 and 𝑄. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = (𝑃𝐿𝑄)) | ||
Theorem | tghilberti1 26351* | There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ran 𝐿(𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
Theorem | tghilberti2 26352* | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ ran 𝐿(𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
Theorem | tglinethrueu 26353* | There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ran 𝐿(𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
Theorem | tglnne0 26354 | A line 𝐴 has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
Theorem | tglnpt2 26355* | Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) | ||
Theorem | tglineintmo 26356* | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | tglineineq 26357 | Two distinct lines intersect in at most one point, variation. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | tglineneq 26358 | Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) | ||
Theorem | tglineinteq 26359 | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐿𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐿𝐷)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | ncolncol 26360 | Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝐷 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | ||
Theorem | coltr 26361 | A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶)) & ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
Theorem | coltr3 26362 | A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶)) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐿𝐶)) | ||
Theorem | colline 26363* | Three points are colinear iff there is a line through all three of them. Theorem 6.23 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 28-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) ⇒ ⊢ (𝜑 → ((𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍) ↔ ∃𝑎 ∈ ran 𝐿(𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎))) | ||
Theorem | tglowdim2l 26364* | Reformulation of the lower dimension axiom for dimension two. There exist three non-colinear points. Theorem 6.24 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ¬ (𝑐 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏)) | ||
Theorem | tglowdim2ln 26365* | There is always one point outside of any line. Theorem 6.25 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 16-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 ¬ 𝑐 ∈ (𝐴𝐿𝐵)) | ||
Syntax | cmir 26366 | Declare the constant for the point inversion function. |
class pInvG | ||
Definition | df-mir 26367* | Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 26369 and ismir 26373. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))))) | ||
Theorem | mirreu3 26368* | Existential uniqueness of the mirror point. Theorem 7.8 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃!𝑏 ∈ 𝑃 ((𝑀 − 𝑏) = (𝑀 − 𝐴) ∧ 𝑀 ∈ (𝑏𝐼𝐴))) | ||
Theorem | mirval 26369* | Value of the point inversion function 𝑆. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑆‘𝐴) = (𝑦 ∈ 𝑃 ↦ (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝑦) ∧ 𝐴 ∈ (𝑧𝐼𝑦))))) | ||
Theorem | mirfv 26370* | Value of the point inversion function 𝑀. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘𝐵) = (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)))) | ||
Theorem | mircgr 26371 | Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | mirbtwn 26372 | Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)) | ||
Theorem | ismir 26373 | Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐴 − 𝐵)) & ⊢ (𝜑 → 𝐴 ∈ (𝐶𝐼𝐵)) ⇒ ⊢ (𝜑 → 𝐶 = (𝑀‘𝐵)) | ||
Theorem | mirf 26374 | Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) ⇒ ⊢ (𝜑 → 𝑀:𝑃⟶𝑃) | ||
Theorem | mircl 26375 | Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃) | ||
Theorem | mirmir 26376 | The point inversion function is an involution. Theorem 7.7 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘(𝑀‘𝐵)) = 𝐵) | ||
Theorem | mircom 26377 | Variation on mirmir 26376. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → (𝑀‘𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝑀‘𝐶) = 𝐵) | ||
Theorem | mirreu 26378* | Any point has a unique antecedent through point inversion. Theorem 7.8 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃!𝑎 ∈ 𝑃 (𝑀‘𝑎) = 𝐵) | ||
Theorem | mireq 26379 | Equality deduction for point inversion. Theorem 7.9 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝑀‘𝐵) = (𝑀‘𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | mirinv 26380 | The only invariant point of a point inversion Theorem 7.3 of [Schwabhauser] p. 49, Theorem 7.10 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑀‘𝐵) = 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | mirne 26381 | Mirror of non-center point cannot be the center point. (Contributed by Thierry Arnoux, 27-Sep-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ≠ 𝐴) ⇒ ⊢ (𝜑 → (𝑀‘𝐵) ≠ 𝐴) | ||
Theorem | mircinv 26382 | The center point is invariant of a point inversion. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) = 𝐴) | ||
Theorem | mirf1o 26383 | The point inversion function 𝑀 is a bijection. Theorem 7.11 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) ⇒ ⊢ (𝜑 → 𝑀:𝑃–1-1-onto→𝑃) | ||
Theorem | miriso 26384 | The point inversion function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 7.13 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) | ||
Theorem | mirbtwni 26385 | Point inversion preserves betweenness, first half of Theorem 7.15 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) ⇒ ⊢ (𝜑 → (𝑀‘𝑌) ∈ ((𝑀‘𝑋)𝐼(𝑀‘𝑍))) | ||
Theorem | mirbtwnb 26386 | Point inversion preserves betweenness. Theorem 7.15 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐼𝑍) ↔ (𝑀‘𝑌) ∈ ((𝑀‘𝑋)𝐼(𝑀‘𝑍)))) | ||
Theorem | mircgrs 26387 | Point inversion preserves congruence. Theorem 7.16 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑇)) ⇒ ⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = ((𝑀‘𝑍) − (𝑀‘𝑇))) | ||
Theorem | mirmir2 26388 | Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘((𝑆‘𝑌)‘𝑋)) = ((𝑆‘(𝑀‘𝑌))‘(𝑀‘𝑋))) | ||
Theorem | mirmot 26389 | Point investion is a motion of the geometric space. Theorem 7.14 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝐺Ismt𝐺)) | ||
Theorem | mirln 26390 | If two points are on the same line, so is the mirror point of one through the other. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝐷) | ||
Theorem | mirln2 26391 | If a point and its mirror point are both on the same line, so is the center of the point inversion. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐷) | ||
Theorem | mirconn 26392 | Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼𝑋))) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) | ||
Theorem | mirhl 26393 | If two points 𝑋 and 𝑌 are on the same half-line from 𝑍, the same applies to the mirror points. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(𝐾‘𝑍)𝑌) ⇒ ⊢ (𝜑 → (𝑀‘𝑋)(𝐾‘(𝑀‘𝑍))(𝑀‘𝑌)) | ||
Theorem | mirbtwnhl 26394 | If the center of the point inversion 𝐴 is between two points 𝑋 and 𝑌, then the half lines are mirrored. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝐴) & ⊢ (𝜑 → 𝑌 ≠ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝑍(𝐾‘𝐴)𝑋 ↔ (𝑀‘𝑍)(𝐾‘𝐴)𝑌)) | ||
Theorem | mirhl2 26395 | Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝐴) & ⊢ (𝜑 → 𝑌 ≠ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) ⇒ ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝑌) | ||
Theorem | mircgrextend 26396 | Link congruence over a pair of mirror points. cf tgcgrextend 26199. (Contributed by Thierry Arnoux, 4-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ 𝑀 = (𝑆‘𝐵) & ⊢ 𝑁 = (𝑆‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝑋 − 𝑌)) ⇒ ⊢ (𝜑 → (𝐴 − (𝑀‘𝐴)) = (𝑋 − (𝑁‘𝑋))) | ||
Theorem | mirtrcgr 26397 | Point inversion of one point of a triangle around another point preserves triangle congruence. (Contributed by Thierry Arnoux, 4-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ 𝑀 = (𝑆‘𝐵) & ⊢ 𝑁 = (𝑆‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝑋𝑌𝑍”〉) ⇒ ⊢ (𝜑 → 〈“(𝑀‘𝐴)𝐵𝐶”〉 ∼ 〈“(𝑁‘𝑋)𝑌𝑍”〉) | ||
Theorem | mirauto 26398 | Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑇) & ⊢ 𝑋 = (𝑀‘𝐴) & ⊢ 𝑌 = (𝑀‘𝐵) & ⊢ 𝑍 = (𝑀‘𝐶) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐵) = 𝐶) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 𝑍) | ||
Theorem | miduniq 26399 | Uniqueness of the middle point, expressed with point inversion. Theorem 7.17 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑋) = 𝑌) & ⊢ (𝜑 → ((𝑆‘𝐵)‘𝑋) = 𝑌) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | miduniq1 26400 | Uniqueness of the middle point, expressed with point inversion. Theorem 7.18 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑋) = ((𝑆‘𝐵)‘𝑋)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |