Home | Metamath
Proof Explorer Theorem List (p. 254 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlne2 25301 | The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | hlln 25302 | 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 25303 | The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝐵) | ||
Theorem | hlid 25304 | 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 25305 | 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 25306 | Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ (𝐶𝐼𝐵)) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐷 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐴(𝐾‘𝐶)𝐷)) | ||
Theorem | btwnhl1 25307 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → 𝐶(𝐾‘𝐴)𝐵) | ||
Theorem | btwnhl2 25308 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐴) | ||
Theorem | btwnhl 25309 | Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐼𝐶)) | ||
Theorem | lnhl 25310 | 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 25311* | 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 25312 | Lemma for hlcgreu 25313. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐷 ≠ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝐷) & ⊢ (𝜑 → 𝑌(𝐾‘𝐴)𝐷) & ⊢ (𝜑 → (𝐴 − 𝑋) = (𝐵 − 𝐶)) & ⊢ (𝜑 → (𝐴 − 𝑌) = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | hlcgreu 25313* | The point constructed in hlcgrex 25311 is unique. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ − = (dist‘𝐺) & ⊢ (𝜑 → 𝐷 ≠ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑃 (𝑥(𝐾‘𝐴)𝐷 ∧ (𝐴 − 𝑥) = (𝐵 − 𝐶))) | ||
Theorem | btwnlng1 25314 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | btwnlng2 25315 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | btwnlng3 25316 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) ⇒ ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) | ||
Theorem | lncom 25317 | 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 25318 | 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 25319 | 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 25320 | Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
Theorem | ncolne2 25321 | Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) TODO (NM): maybe ncolne2 25321 could be simplified out and deleted, replaced by ncolcom 25256. |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑍) | ||
Theorem | tgisline 25322* | 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 25323 | It takes two different points to form a line. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
Theorem | tglndim0 25324 | There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → (#‘𝐵) = 1) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ ran 𝐿) | ||
Theorem | tgelrnln 25325 | 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 25326 | Transitivity law for lines, one half of tglineelsb2 25327. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ≠ 𝑄) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ≠ 𝑃) & ⊢ (𝜑 → 𝑆 ∈ (𝑃𝐿𝑄)) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑆)) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑄)) | ||
Theorem | tglineelsb2 25327 | 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 25328 | 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 25329 | 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 25330 | 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 25331 | 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 25332* | 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 25333* | 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 25334* | 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 25335 | A line 𝐴 has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
Theorem | tglnpt2 25336* | Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) | ||
Theorem | tglineintmo 25337* | 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 25338 | 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 25339 | Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷)) | ||
Theorem | tglineinteq 25340 | 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 25341 | Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝐷 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | ||
Theorem | coltr 25342 | A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶)) & ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷)) | ||
Theorem | coltr3 25343 | A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶)) & ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐿𝐶)) | ||
Theorem | colline 25344* | 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 25345* | Reformulation of the lower dimension axiom for dimension 2. 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 25346* | 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 25347 | Declare the constant for the point inversion function. |
class pInvG | ||
Definition | df-mir 25348* | Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 25350 and ismir 25354. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))))) | ||
Theorem | mirreu3 25349* | 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 25350* | 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 25351* | 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 25352 | 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 25353 | 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 25354 | 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 25355 | Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) ⇒ ⊢ (𝜑 → 𝑀:𝑃⟶𝑃) | ||
Theorem | mircl 25356 | Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃) | ||
Theorem | mirmir 25357 | 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 25358 | Variation on mirmir 25357. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → (𝑀‘𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝑀‘𝐶) = 𝐵) | ||
Theorem | mirreu 25359* | 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 25360 | 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 25361 | 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 25362 | 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 25363 | The center point is invariant of a point inversion. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) = 𝐴) | ||
Theorem | mirf1o 25364 | 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 25365 | 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 25366 | 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 25367 | 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 25368 | 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 25369 | Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘((𝑆‘𝑌)‘𝑋)) = ((𝑆‘(𝑀‘𝑌))‘(𝑀‘𝑋))) | ||
Theorem | mirmot 25370 | 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 25371 | 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 25372 | 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 25373 | Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼𝑋))) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) | ||
Theorem | mirhl 25374 | 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 25375 | 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 25376 | Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝐴) & ⊢ (𝜑 → 𝑌 ≠ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) ⇒ ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝑌) | ||
Theorem | mircgrextend 25377 | Link congruence over a pair of mirror points. cf tgcgrextend 25180. (Contributed by Thierry Arnoux, 4-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ 𝑀 = (𝑆‘𝐵) & ⊢ 𝑁 = (𝑆‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝑋 − 𝑌)) ⇒ ⊢ (𝜑 → (𝐴 − (𝑀‘𝐴)) = (𝑋 − (𝑁‘𝑋))) | ||
Theorem | mirtrcgr 25378 | 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 25379 | Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑇) & ⊢ 𝑋 = (𝑀‘𝐴) & ⊢ 𝑌 = (𝑀‘𝐵) & ⊢ 𝑍 = (𝑀‘𝐶) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐵) = 𝐶) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 𝑍) | ||
Theorem | miduniq 25380 | Unicity 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 25381 | Unicity 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) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑋) = ((𝑆‘𝐵)‘𝑋)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | miduniq2 25382 | If two point inversions commute, they are identical. Theorem 7.19 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘((𝑆‘𝐵)‘𝑋)) = ((𝑆‘𝐵)‘((𝑆‘𝐴)‘𝑋))) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | colmid 25383 | Colinearity and equidistance implies midpoint. Theorem 7.20 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) & ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑋 − 𝐵)) ⇒ ⊢ (𝜑 → (𝐵 = (𝑀‘𝐴) ∨ 𝐴 = 𝐵)) | ||
Theorem | symquadlem 25384 | Lemma of the symetrial quadrilateral. The diagonals of quadrilaterals with congruent opposing sides intersect at their middle point. In Euclidean geometry, such quadrilaterals are called parallelograms, as opposing sides are parallel. However, this is not necessarily true in the case of absolute geometry. Lemma 7.21 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → 𝐵 ≠ 𝐷) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐷 − 𝐴)) & ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) & ⊢ (𝜑 → (𝑋 ∈ (𝐵𝐿𝐷) ∨ 𝐵 = 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 = (𝑀‘𝐶)) | ||
Theorem | krippenlem 25385 | Lemma for krippen 25386. We can assume krippen.7 "without loss of generality" (Contributed by Thierry Arnoux, 12-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑋) & ⊢ 𝑁 = (𝑆‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵)) & ⊢ (𝜑 → (𝐶 − 𝐸) = (𝐶 − 𝐹)) & ⊢ (𝜑 → 𝐵 = (𝑀‘𝐴)) & ⊢ (𝜑 → 𝐹 = (𝑁‘𝐸)) & ⊢ ≤ = (≤G‘𝐺) & ⊢ (𝜑 → (𝐶 − 𝐴) ≤ (𝐶 − 𝐸)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝑋𝐼𝑌)) | ||
Theorem | krippen 25386 | Krippenlemma (German for crib's lemma) Lemma 7.22 of [Schwabhauser] p. 53. proven by Gupta 1965 as Theorem 3.45. (Contributed by Thierry Arnoux, 12-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑋) & ⊢ 𝑁 = (𝑆‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐸)) & ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐹)) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵)) & ⊢ (𝜑 → (𝐶 − 𝐸) = (𝐶 − 𝐹)) & ⊢ (𝜑 → 𝐵 = (𝑀‘𝐴)) & ⊢ (𝜑 → 𝐹 = (𝑁‘𝐸)) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝑋𝐼𝑌)) | ||
Theorem | midexlem 25387* | Lemma for the existence of a middle point. Lemma 7.25 of [Schwabhauser] p. 55. This proof of the existence of a midpoint requires the existence of a third point 𝐶 equidistant to 𝐴 and 𝐵 This condition will be removed later. Because the operation notation (𝐴(midG‘𝐺)𝐵) for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation 𝐵 = (𝑀‘𝐴) has to be used. See mideu 25430 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑥) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴)) | ||
Syntax | crag 25388 | Declare the constant for the class of right angles. |
class ∟G | ||
Definition | df-rag 25389* | Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 25392. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}) | ||
Syntax | cperpg 25390 | Declare the constant for the perpendicular relation. |
class ⟂G | ||
Definition | df-perpg 25391* | Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 25407. (Contributed by Thierry Arnoux, 8-Sep-2019.) |
⊢ ⟂G = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔))}) | ||
Theorem | israg 25392 | Property for 3 points A, B, C to form a right angle. Definition 8.1 of [Schwabhauser] p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝐴 − 𝐶) = (𝐴 − ((𝑆‘𝐵)‘𝐶)))) | ||
Theorem | ragcom 25393 | Commutative rule for right angles. Theorem 8.2 of [Schwabhauser] p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 〈“𝐶𝐵𝐴”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragcol 25394 | The right angle property is independent of the choice of point on one side. Theorem 8.3 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → (𝐴 ∈ (𝐵𝐿𝐷) ∨ 𝐵 = 𝐷)) ⇒ ⊢ (𝜑 → 〈“𝐷𝐵𝐶”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragmir 25395 | Right angle property is preserved by point inversion. Theorem 8.4 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵((𝑆‘𝐵)‘𝐶)”〉 ∈ (∟G‘𝐺)) | ||
Theorem | mirrag 25396 | Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ 𝑀 = (𝑆‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → 〈“(𝑀‘𝐴)(𝑀‘𝐵)(𝑀‘𝐶)”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragtrivb 25397 | Trivial right angle. Theorem 8.5 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐵”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragflat2 25398 | Deduce equality from two right angles. Theorem 8.6 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐷𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | ragflat 25399 | Deduce equality from two right angles. Theorem 8.7 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐴𝐶𝐵”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | ragtriva 25400 | Trivial right angle. Theorem 8.8 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐴”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |