| Metamath
Proof Explorer Theorem List (p. 286 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | tgbtwnintr 28501 | 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 28502 | 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 28503 | 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 28504 | 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 28505 | 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 28506 | 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 28507* | 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 28508* | 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 28509* | Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝑃 𝑋 ≠ 𝑦) | ||
| Theorem | tgldimor 28510 | Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
| ⊢ 𝑃 = (𝐸‘𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤ (♯‘𝑃))) | ||
| Theorem | tgldim0eq 28511 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
| ⊢ 𝑃 = (𝐸‘𝐹) & ⊢ (𝜑 → (♯‘𝑃) = 1) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | tgldim0itv 28512 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (♯‘𝑃) = 1) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶)) | ||
| Theorem | tgldim0cgr 28513 | In dimension zero, any two pairs of points are congruent. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (♯‘𝑃) = 1) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) | ||
| Theorem | tgbtwndiff 28514* | 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 28515 | In geometries of dimension less than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) | ||
| Theorem | tgifscgr 28516 | 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 28517 | 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 28518 | Declare the constant for the congruence between shapes relation. |
| class cgrG | ||
| Definition | df-cgrg 28519* |
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 28816 and expanded in iscgra 28817. This does not mean our system is weaker; dfcgrg2 28871 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 28528, cgr3simp2 28529, cgr3simp3 28530, cgrcgra 28829, and permutation laws such as cgr3swap12 28531 and dfcgrg2 28871. Ideally, we would define this for functions of any set, but we will use words (see df-word 14553) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
| ⊢ cgrG = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}) | ||
| Theorem | iscgrg 28520* | 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 28521* | 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 28522* | 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 28523 | The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉 ↔ ((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)))) | ||
| Theorem | trgcgr 28524 | Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) | ||
| Theorem | ercgrg 28525 | 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 28526* | 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 28527 | Reflexivity law for three-place congruence. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐴𝐵𝐶”〉) | ||
| Theorem | cgr3simp1 28528 | 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 28529 | 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 28530 | 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 28531 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐵𝐴𝐶”〉 ∼ 〈“𝐸𝐷𝐹”〉) | ||
| Theorem | cgr3swap23 28532 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐶𝐵”〉 ∼ 〈“𝐷𝐹𝐸”〉) | ||
| Theorem | cgr3swap13 28533 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 3-Oct-2020.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉 ∼ 〈“𝐹𝐸𝐷”〉) | ||
| Theorem | cgr3rotr 28534 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉 ∼ 〈“𝐹𝐷𝐸”〉) | ||
| Theorem | cgr3rotl 28535 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐵𝐶𝐴”〉 ∼ 〈“𝐸𝐹𝐷”〉) | ||
| Theorem | trgcgrcom 28536 | Commutative law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∼ 〈“𝐴𝐵𝐶”〉) | ||
| Theorem | cgr3tr 28537 | Transitivity law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐾 ∈ 𝑃) & ⊢ (𝜑 → 𝐿 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∼ 〈“𝐽𝐾𝐿”〉) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐽𝐾𝐿”〉) | ||
| Theorem | tgbtwnxfr 28538 | 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 28539 | 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 28540 | Declare the constant for the isometry builder. |
| class Ismt | ||
| Definition | df-ismt 28541* | Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 28542. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
| ⊢ Ismt = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))}) | ||
| Theorem | isismt 28542* | Property of being an isometry. Compare with isismty 37808. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑃 = (Base‘𝐻) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ − = (dist‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏)))) | ||
| Theorem | ismot 28543* | 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 28544 | Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐵)) = (𝐴 − 𝐵)) | ||
| Theorem | idmot 28545 | The identity is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( I ↾ 𝑃) ∈ (𝐺Ismt𝐺)) | ||
| Theorem | motf1o 28546 | Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → 𝐹:𝑃–1-1-onto→𝑃) | ||
| Theorem | motcl 28547 | Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑃) | ||
| Theorem | motco 28548 | The composition of two motions is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐺Ismt𝐺)) | ||
| Theorem | cnvmot 28549 | The converse of a motion is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) ⇒ ⊢ (𝜑 → ◡𝐹 ∈ (𝐺Ismt𝐺)) | ||
| Theorem | motplusg 28550* | 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 28551* | 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 28552* | 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 28553 | 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 28554* | 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 28555 | Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → 𝐿 Fn ((𝑃 × 𝑃) ∖ I )) | ||
| Theorem | tglnunirn 28556 | Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) ⇒ ⊢ (𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃) | ||
| Theorem | tglnpt 28557 | Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑃) | ||
| Theorem | tglngne 28558 | It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
| Theorem | tglngval 28559* | The line going through points 𝑋 and 𝑌. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) ⇒ ⊢ (𝜑 → (𝑋𝐿𝑌) = {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))}) | ||
| Theorem | tglnssp 28560 | 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 28561 | 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 28562 | 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 28563 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
| Theorem | btwncolg2 28564 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
| Theorem | btwncolg3 28565 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) | ||
| Theorem | colcom 28566 | 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 28567 | 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 28568 | 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 28569 | Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋)) | ||
| Theorem | ncolrot1 28570 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) | ||
| Theorem | ncolrot2 28571 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → ¬ (𝑌 ∈ (𝑍𝐿𝑋) ∨ 𝑍 = 𝑋)) | ||
| Theorem | tgdim01ln 28572 | 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 28573 | If there are three non-colinear points, then the dimension is at least two. Converse of tglowdim2l 28658. (Contributed by Thierry Arnoux, 23-Feb-2020.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌)) ⇒ ⊢ (𝜑 → 𝐺DimTarskiG≥2) | ||
| Theorem | lnxfr 28574 | 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 28575* | 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 28576 | 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 28577 | 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 28578 | 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 28579 | 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 28580 | Lemma for tgbtwnconn1 28583. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) ⇒ ⊢ (𝜑 → 𝐻 = 𝐽) | ||
| Theorem | tgbtwnconn1lem2 28581 | Lemma for tgbtwnconn1 28583. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 − 𝐹) = (𝐶 − 𝐷)) | ||
| Theorem | tgbtwnconn1lem3 28582 | Lemma for tgbtwnconn1 28583. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐽 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) & ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) & ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐼𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐷𝐼𝐹)) & ⊢ (𝜑 → 𝐶 ≠ 𝐸) ⇒ ⊢ (𝜑 → 𝐷 = 𝐹) | ||
| Theorem | tgbtwnconn1 28583 | 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 28584 | Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))) | ||
| Theorem | tgbtwnconn3 28585 | Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) | ||
| Theorem | tgbtwnconnln3 28586 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) & ⊢ 𝐿 = (LineG‘𝐺) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) | ||
| Theorem | tgbtwnconn22 28587 | Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) & ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐸)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝐷𝐼𝐸)) | ||
| Theorem | tgbtwnconnln1 28588 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
| Theorem | tgbtwnconnln2 28589 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
| Syntax | cleg 28590 | Less-than relation for geometric congruences. |
| class ≤G | ||
| Definition | df-leg 28591* | Define the less-than relationship between geometric distance congruence classes. See legval 28592. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
| ⊢ ≤G = (𝑔 ∈ V ↦ {〈𝑒, 𝑓〉 ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))}) | ||
| Theorem | legval 28592* | Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ≤ = {〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))}) | ||
| Theorem | legov 28593* | 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 28594* | 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 28595 | 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 28596 | Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐶)) | ||
| Theorem | legtrd 28597 | 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 28598 | 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 28599 | 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 28600 | 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) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴 − 𝐴) ≤ (𝐶 − 𝐷)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |