Home | Metamath
Proof Explorer Theorem List (p. 255 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 | ragflat3 25401 | Right angle and colinearity. Theorem 8.9 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 4-Sep-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ∨ 𝐶 = 𝐵)) | ||
Theorem | ragcgr 25402 | Right angle and colinearity. Theorem 8.10 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 4-Sep-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∼ 〈“𝐷𝐸𝐹”〉) ⇒ ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) | ||
Theorem | motrag 25403 | Right angles are preserved by motions. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 〈“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragncol 25404 | Right angle implies non-colinearity. A consequence of theorem 8.9 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | ||
Theorem | perpln1 25405 | Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) | ||
Theorem | perpln2 25406 | Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) | ||
Theorem | isperp 25407* | Property for 2 lines A, B to be perpendicular. Item (ii) of definition 8.11 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) | ||
Theorem | perpcom 25408 | The "perpendicular" relation commutes. Theorem 8.12 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 𝐵(⟂G‘𝐺)𝐴) | ||
Theorem | perpneq 25409 | Two perpendicular lines are different. Theorem 8.14 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | isperp2 25410* | Property for 2 lines A, B, intersecting at a point X to be perpendicular. Item (i) of definition 8.13 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑋𝑣”〉 ∈ (∟G‘𝐺))) | ||
Theorem | isperp2d 25411 | One direction of isperp2 25410. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 〈“𝑈𝑋𝑉”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragperp 25412 | Deduce that two lines are perpendicular from a right angle statement. One direction of theorem 8.13 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 20-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ≠ 𝑋) & ⊢ (𝜑 → 𝑉 ≠ 𝑋) & ⊢ (𝜑 → 〈“𝑈𝑋𝑉”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) | ||
Theorem | footex 25413* | Lemma for foot 25414: existence part. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) | ||
Theorem | foot 25414* | From a point 𝐶 outside of a line 𝐴, there exists a unique point 𝑥 on 𝐴 such that (𝐶𝐿𝑥) is perpendicular to 𝐴. That point is called the foot from 𝐶 on 𝐴. Theorem 8.18 of [Schwabhauser] p. 60. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) | ||
Theorem | footne 25415 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐴) | ||
Theorem | footeq 25416 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴) & ⊢ (𝜑 → (𝑌𝐿𝑍)(⟂G‘𝐺)𝐴) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | hlperpnel 25417 | A point on a half-line which is perpendicular to a line cannot be on that line. (Contributed by Thierry Arnoux, 1-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)(𝑈𝐿𝑉)) & ⊢ (𝜑 → 𝑉(𝐾‘𝑈)𝑊) ⇒ ⊢ (𝜑 → ¬ 𝑊 ∈ 𝐴) | ||
Theorem | perprag 25418 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝐷)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐶𝐷”〉 ∈ (∟G‘𝐺)) | ||
Theorem | perpdragALT 25419 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐵𝐿𝐶)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) | ||
Theorem | perpdrag 25420 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐵𝐿𝐶)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) | ||
Theorem | colperp 25421 | Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)𝐷) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴𝐿𝐶)(⟂G‘𝐺)𝐷) | ||
Theorem | colperpexlem1 25422 | Lemma for colperp 25421. First part of lemma 8.20 of [Schwabhauser] p. 62. (Contributed by Thierry Arnoux, 27-Oct-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ 𝑁 = (𝑆‘𝐵) & ⊢ 𝐾 = (𝑆‘𝑄) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐾‘(𝑀‘𝐶)) = (𝑁‘𝐶)) ⇒ ⊢ (𝜑 → 〈“𝐵𝐴𝑄”〉 ∈ (∟G‘𝐺)) | ||
Theorem | colperpexlem2 25423 | Lemma for colperpex 25425. Second part of lemma 8.20 of [Schwabhauser] p. 62. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ 𝑁 = (𝑆‘𝐵) & ⊢ 𝐾 = (𝑆‘𝑄) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐾‘(𝑀‘𝐶)) = (𝑁‘𝐶)) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝑄) | ||
Theorem | colperpexlem3 25424* | Lemma for colperpex 25425. Case 1 of theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴𝐿𝐵)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ∃𝑡 ∈ 𝑃 ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝐶𝐼𝑝)))) | ||
Theorem | colperpex 25425* | In dimension 2 and above, on a line (𝐴𝐿𝐵) there is always a perpendicular 𝑃 from 𝐴 on a given plane (here given by 𝐶, in case 𝐶 does not lie on the line). Theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)(𝐴𝐿𝐵) ∧ ∃𝑡 ∈ 𝑃 ((𝑡 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ∧ 𝑡 ∈ (𝐶𝐼𝑝)))) | ||
Theorem | mideulem2 25426 | Lemma for opphllem 25427, which is itself used for mideu 25430. (Contributed by Thierry Arnoux, 19-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑂 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵)) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂)) & ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂)) & ⊢ (𝜑 → 𝑅 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄)) & ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝑇𝐼𝐵)) & ⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂)) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍)) & ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅)) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍)) ⇒ ⊢ (𝜑 → 𝐵 = 𝑀) | ||
Theorem | opphllem 25427* | Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 25428 and later for opphl 25446. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑂 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵)) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂)) & ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂)) & ⊢ (𝜑 → 𝑅 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄)) & ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝐵 = ((𝑆‘𝑥)‘𝐴) ∧ 𝑂 = ((𝑆‘𝑥)‘𝑅))) | ||
Theorem | mideulem 25428* | Lemma for mideu 25430. We can assume mideulem.9 "without loss of generality" (Contributed by Thierry Arnoux, 25-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑂 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵)) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂)) & ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂)) & ⊢ (𝜑 → (𝐴 − 𝑂)(≤G‘𝐺)(𝐵 − 𝑄)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = ((𝑆‘𝑥)‘𝐴)) | ||
Theorem | midex 25429* | Existence of the midpoint, part Theorem 8.22 of [Schwabhauser] p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = ((𝑆‘𝑥)‘𝐴)) | ||
Theorem | mideu 25430* | Existence and uniqueness of the midpoint, Theorem 8.22 of [Schwabhauser] p. 64. (Contributed by Thierry Arnoux, 25-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑃 𝐵 = ((𝑆‘𝑥)‘𝐴)) | ||
Theorem | islnopp 25431* | The property for two points 𝐴 and 𝐵 to lie on the opposite sides of a set 𝐷 Definition 9.1 of [Schwabhauser] p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)))) | ||
Theorem | islnoppd 25432* | Deduce that 𝐴 and 𝐵 lie on opposite sides of line 𝐿. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) ⇒ ⊢ (𝜑 → 𝐴𝑂𝐵) | ||
Theorem | oppne1 25433* | Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) | ||
Theorem | oppne2 25434* | Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) | ||
Theorem | oppne3 25435* | Points lying on opposite sides of a line cannot be equal. (Contributed by Thierry Arnoux, 3-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | oppcom 25436* | Commutativity rule for "opposite" Theorem 9.2 of [Schwabhauser] p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑂𝐴) | ||
Theorem | opptgdim2 25437* | If two points opposite to a line exist, dimension must be 2 or more. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐵) ⇒ ⊢ (𝜑 → 𝐺DimTarskiG≥2) | ||
Theorem | oppnid 25438* | The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑂𝐴) | ||
Theorem | opphllem1 25439* | Lemma for opphl 25446. (Contributed by Thierry Arnoux, 20-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝑀 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 = (𝑆‘𝐶)) & ⊢ (𝜑 → 𝐴 ≠ 𝑅) & ⊢ (𝜑 → 𝐵 ≠ 𝑅) & ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐴)) ⇒ ⊢ (𝜑 → 𝐵𝑂𝐶) | ||
Theorem | opphllem2 25440* | Lemma for opphl 25446. Lemma 9.3 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝑀 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 = (𝑆‘𝐶)) & ⊢ (𝜑 → 𝐴 ≠ 𝑅) & ⊢ (𝜑 → 𝐵 ≠ 𝑅) & ⊢ (𝜑 → (𝐴 ∈ (𝑅𝐼𝐵) ∨ 𝐵 ∈ (𝑅𝐼𝐴))) ⇒ ⊢ (𝜑 → 𝐵𝑂𝐶) | ||
Theorem | opphllem3 25441* | Lemma for opphl 25446: We assume opphllem3.l "without loss of generality". (Contributed by Thierry Arnoux, 21-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ 𝑁 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝐷) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) & ⊢ (𝜑 → 𝑅 ≠ 𝑆) & ⊢ (𝜑 → (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → (𝑁‘𝑅) = 𝑆) ⇒ ⊢ (𝜑 → (𝑈(𝐾‘𝑅)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) | ||
Theorem | opphllem4 25442* | Lemma for opphl 25446. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ 𝑁 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝐷) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) & ⊢ (𝜑 → 𝑅 ≠ 𝑆) & ⊢ (𝜑 → (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → (𝑁‘𝑅) = 𝑆) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈(𝐾‘𝑅)𝐴) & ⊢ (𝜑 → 𝑉(𝐾‘𝑆)𝐶) ⇒ ⊢ (𝜑 → 𝑈𝑂𝑉) | ||
Theorem | opphllem5 25443* | Second part of Lemma 9.4 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ 𝑁 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝐷) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈(𝐾‘𝑅)𝐴) & ⊢ (𝜑 → 𝑉(𝐾‘𝑆)𝐶) ⇒ ⊢ (𝜑 → 𝑈𝑂𝑉) | ||
Theorem | opphllem6 25444* | First part of Lemma 9.4 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ 𝑁 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝐷) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → (𝑁‘𝑅) = 𝑆) ⇒ ⊢ (𝜑 → (𝑈(𝐾‘𝑅)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) | ||
Theorem | oppperpex 25445* | Restating colperpex 25425 using the "opposite side of a line" relation. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 ((𝐴𝐿𝑝)(⟂G‘𝐺)𝐷 ∧ 𝐶𝑂𝑝)) | ||
Theorem | opphl 25446* | If two points 𝐴 and 𝐶 lie on the opposite side of a line 𝐷 then any point of the half line (𝑅 𝐴) also lies opposite to 𝐶. Theorem 9.5 of [Schwabhauser] p. 69. (Contributed by Thierry Arnoux, 3-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝐴(𝐾‘𝑅)𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑂𝐶) | ||
Theorem | outpasch 25447* | Axiom of Pasch, outer form. This was proven by Gupta from other axioms and is therefore presented as Theorem 9.6 in [Schwabhauser] p. 70. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝑃) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝑅)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵𝐼𝐶)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))) | ||
Theorem | hlpasch 25448* | An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶)) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))) | ||
Syntax | chpg 25449 | "Belong to the same open half-plane" relation for points in a geometry. |
class hpG | ||
Definition | df-hpg 25450* | Define the open half plane relation for a geometry 𝐺. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 25452 to find the same formulation. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))})) | ||
Theorem | ishpg 25451* | Value of the half-plane relation for a given line 𝐷. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)}) | ||
Theorem | hpgbr 25452* | Half-planes : property for points 𝐴 and 𝐵 to belong to the same open half plane delimited by line 𝐷. Definition 9.7 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ ∃𝑐 ∈ 𝑃 (𝐴𝑂𝑐 ∧ 𝐵𝑂𝑐))) | ||
Theorem | hpgne1 25453* | Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴((hpG‘𝐺)‘𝐷)𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) | ||
Theorem | hpgne2 25454* | Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴((hpG‘𝐺)‘𝐷)𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) | ||
Theorem | lnopp2hpgb 25455* | Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) ⇒ ⊢ (𝜑 → (𝐵𝑂𝐶 ↔ 𝐴((hpG‘𝐺)‘𝐷)𝐵)) | ||
Theorem | lnoppnhpg 25456* | If two points lie on the opposite side of a line 𝐷, they are not on the same half-plane. Theorem 9.9 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴((hpG‘𝐺)‘𝐷)𝐵) | ||
Theorem | hpgerlem 25457* | Lemma for the proof that the half-plane relation is an equivalence relation. Lemma 9.10 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 𝐴𝑂𝑐) | ||
Theorem | hpgid 25458* | The half-plane relation is reflexive. Theorem 9.11 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝐴((hpG‘𝐺)‘𝐷)𝐴) | ||
Theorem | hpgcom 25459* | The half-plane relation commutes. Theorem 9.12 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴((hpG‘𝐺)‘𝐷)𝐵) ⇒ ⊢ (𝜑 → 𝐵((hpG‘𝐺)‘𝐷)𝐴) | ||
Theorem | hpgtr 25460* | The half-plane relation is transitive. Theorem 9.13 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴((hpG‘𝐺)‘𝐷)𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐵((hpG‘𝐺)‘𝐷)𝐶) ⇒ ⊢ (𝜑 → 𝐴((hpG‘𝐺)‘𝐷)𝐶) | ||
Theorem | colopp 25461* | Opposite sides of a line for colinear points. Theorem 9.18 of [Schwabhauser] p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴𝑂𝐵 ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∧ ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷))) | ||
Theorem | colhp 25462* | Half-plane relation for colinear points. Theorem 9.19 of [Schwabhauser] p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) & ⊢ 𝐾 = (hlG‘𝐺) ⇒ ⊢ (𝜑 → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ (𝐴(𝐾‘𝐶)𝐵 ∧ ¬ 𝐴 ∈ 𝐷))) | ||
Theorem | hphl 25463* | If two points are on the same half-line with endpoint on a line, they are on the same half-plane defined by this line. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐵(𝐾‘𝐴)𝐶) ⇒ ⊢ (𝜑 → 𝐵((hpG‘𝐺)‘𝐷)𝐶) | ||
Syntax | cmid 25464 | Declare the constant for the midpoint operation. |
class midG | ||
Syntax | clmi 25465 | Declare the constant for the line mirroring function. |
class lInvG | ||
Definition | df-mid 25466* | Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 25470, midbtwn 25471, and midcgr 25472. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
⊢ midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)))) | ||
Definition | df-lmi 25467* | Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 25479. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ lInvG = (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))) | ||
Theorem | midf 25468 | Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → (midG‘𝐺):(𝑃 × 𝑃)⟶𝑃) | ||
Theorem | midcl 25469 | Closure of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐵) ∈ 𝑃) | ||
Theorem | ismidb 25470 | Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐵 = ((𝑆‘𝑀)‘𝐴) ↔ (𝐴(midG‘𝐺)𝐵) = 𝑀)) | ||
Theorem | midbtwn 25471 | Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐵) ∈ (𝐴𝐼𝐵)) | ||
Theorem | midcgr 25472 | Congruence of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵)) | ||
Theorem | midid 25473 | Midpoint of a null segment. (Contributed by Thierry Arnoux, 7-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐴) = 𝐴) | ||
Theorem | midcom 25474 | Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐵) = (𝐵(midG‘𝐺)𝐴)) | ||
Theorem | mirmid 25475 | Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘𝐵)) = (𝑆‘(𝐴(midG‘𝐺)𝐵))) | ||
Theorem | lmieu 25476* | Uniqueness of the line mirror point. Theorem 10.2 of [Schwabhauser] p. 88. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃!𝑏 ∈ 𝑃 ((𝐴(midG‘𝐺)𝑏) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝑏) ∨ 𝐴 = 𝑏))) | ||
Theorem | lmif 25477 | Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝑀:𝑃⟶𝑃) | ||
Theorem | lmicl 25478 | Closure of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑃) | ||
Theorem | islmib 25479 | Property of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐵 = (𝑀‘𝐴) ↔ ((𝐴(midG‘𝐺)𝐵) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)))) | ||
Theorem | lmicom 25480 | The line mirroring function is an involution. Theorem 10.4 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) = 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝐵) = 𝐴) | ||
Theorem | lmilmi 25481 | Line mirroring is an involution. Theorem 10.5 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝑀‘(𝑀‘𝐴)) = 𝐴) | ||
Theorem | lmireu 25482* | Any point has a unique antecedent through line mirroring. Theorem 10.6 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ∃!𝑏 ∈ 𝑃 (𝑀‘𝑏) = 𝐴) | ||
Theorem | lmieq 25483 | Equality deduction for line mirroring. Theorem 10.7 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) = (𝑀‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | lmiinv 25484 | The invariants of the line mirroring lie on the mirror line. Theorem 10.8 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑀‘𝐴) = 𝐴 ↔ 𝐴 ∈ 𝐷)) | ||
Theorem | lmicinv 25485 | The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) = 𝐴) | ||
Theorem | lmimid 25486 | If we have a right angle, then the mirror point is the point inversion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝐵) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝐶) = (𝑆‘𝐶)) | ||
Theorem | lmif1o 25487 | The line mirroring function 𝑀 is a bijection. Theorem 10.9 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝑀:𝑃–1-1-onto→𝑃) | ||
Theorem | lmiisolem 25488 | Lemma for lmiiso 25489. (Contributed by Thierry Arnoux, 14-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑍) & ⊢ 𝑍 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ⇒ ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | lmiiso 25489 | The line mirroring function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 10.10 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) ⇒ ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | lmimot 25490 | Line mirroring is a motion of the geometric space. Theorem 10.11 of [Schwabhauser] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝐺Ismt𝐺)) | ||
Theorem | hypcgrlem1 25491 | Lemma for hypcgr 25493, case where triangles share a cathetus. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ 𝑆 = ((lInvG‘𝐺)‘((𝐴(midG‘𝐺)𝐷)(LineG‘𝐺)𝐵)) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | ||
Theorem | hypcgrlem2 25492 | Lemma for hypcgr 25493, case where triangles share one vertex 𝐵. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ 𝑆 = ((lInvG‘𝐺)‘((𝐶(midG‘𝐺)𝐹)(LineG‘𝐺)𝐵)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | ||
Theorem | hypcgr 25493 | If the catheti of two right-angled triangles are congruent, so is their hypothenuse. Theorem 10.12 of [Schwabhauser] p. 91. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (∟G‘𝐺)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | ||
Theorem | lmiopp 25494* | Line mirroring produces points on the opposite side of the mirroring line. Theorem 10.14 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝐴𝑂(𝑀‘𝐴)) | ||
Theorem | lnperpex 25495* | Existence of a perpendicular to a line 𝐿 at a given point 𝐴. Theorem 10.15 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝑄 ∈ 𝐷) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 (𝐷(⟂G‘𝐺)(𝑝𝐿𝐴) ∧ 𝑝((hpG‘𝐺)‘𝐷)𝑄)) | ||
Theorem | trgcopy 25496* | Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | ||
Theorem | trgcopyeulem 25497* | Lemma for trgcopyeu 25498. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑡 ∈ (𝐷𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑋”〉) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑌”〉) & ⊢ (𝜑 → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) & ⊢ (𝜑 → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | trgcopyeu 25498* | Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: uniqueness part. Second part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) & ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) ⇒ ⊢ (𝜑 → ∃!𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | ||
Syntax | ccgra 25499 | Declare the constant for the congruence between angles relation. |
class cgrA | ||
Definition | df-cgra 25500* | Define the congruence relation bewteen angles. As for triangles we use "words of points". See iscgra 25501 for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020.) |
⊢ cgrA = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |