![]() |
Metamath
Proof Explorer Theorem List (p. 286 of 484) | < 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-30748) |
![]() (30749-32271) |
![]() (32272-48316) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mirln2 28501 | 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 28502 | Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼𝑋))) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) | ||
Theorem | mirhl 28503 | 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 28504 | 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 28505 | Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝐴) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝐴) & ⊢ (𝜑 → 𝑌 ≠ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) ⇒ ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝑌) | ||
Theorem | mircgrextend 28506 | Link congruence over a pair of mirror points. cf tgcgrextend 28309. (Contributed by Thierry Arnoux, 4-Oct-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ ∼ = (cgrG‘𝐺) & ⊢ 𝑀 = (𝑆‘𝐵) & ⊢ 𝑁 = (𝑆‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝑋 − 𝑌)) ⇒ ⊢ (𝜑 → (𝐴 − (𝑀‘𝐴)) = (𝑋 − (𝑁‘𝑋))) | ||
Theorem | mirtrcgr 28507 | 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 28508 | Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑇) & ⊢ 𝑋 = (𝑀‘𝐴) & ⊢ 𝑌 = (𝑀‘𝐵) & ⊢ 𝑍 = (𝑀‘𝐶) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐵) = 𝐶) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 𝑍) | ||
Theorem | miduniq 28509 | Uniqueness of the middle point, expressed with point inversion. Theorem 7.17 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑋) = 𝑌) & ⊢ (𝜑 → ((𝑆‘𝐵)‘𝑋) = 𝑌) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | miduniq1 28510 | Uniqueness of the middle point, expressed with point inversion. Theorem 7.18 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑋) = ((𝑆‘𝐵)‘𝑋)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | miduniq2 28511 | 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 28512 | 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 28513 | 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 28514 | Lemma for krippen 28515. 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 28515 | 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 28516* | 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 28562 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑀 = (𝑆‘𝑥) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴)) | ||
Syntax | crag 28517 | Declare the constant for the class of right angles. |
class ∟G | ||
Definition | df-rag 28518* | Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 28521. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
⊢ ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}) | ||
Syntax | cperpg 28519 | Declare the constant for the perpendicular relation. |
class ⟂G | ||
Definition | df-perpg 28520* | Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 28536. (Contributed by Thierry Arnoux, 8-Sep-2019.) |
⊢ ⟂G = (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝑔))}) | ||
Theorem | israg 28521 | 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 28522 | 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 28523 | 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 28524 | 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 28525 | Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) & ⊢ 𝑀 = (𝑆‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) ⇒ ⊢ (𝜑 → 〈“(𝑀‘𝐴)(𝑀‘𝐵)(𝑀‘𝐶)”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragtrivb 28526 | 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 28527 | 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 28528 | 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 28529 | Trivial right angle. Theorem 8.8 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 〈“𝐴𝐵𝐴”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ragflat3 28530 | 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 28531 | 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 28532 | Right angles are preserved by motions. (Contributed by Thierry Arnoux, 16-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) & ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) ⇒ ⊢ (𝜑 → 〈“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragncol 28533 | 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 28534 | Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) | ||
Theorem | perpln2 28535 | Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) | ||
Theorem | isperp 28536* | 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 28537 | 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 28538 | 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 28539* | 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 28540 | One direction of isperp2 28539. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐵 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) ⇒ ⊢ (𝜑 → 〈“𝑈𝑋𝑉”〉 ∈ (∟G‘𝐺)) | ||
Theorem | ragperp 28541 | 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 | footexALT 28542* | Alternative version of footex 28545 which minimization requires a notably long time. (Contributed by Thierry Arnoux, 19-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) | ||
Theorem | footexlem1 28543 | Lemma for footex 28545. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 = (𝐸𝐿𝐹)) & ⊢ (𝜑 → 𝐸 ≠ 𝐹) & ⊢ (𝜑 → 𝐸 ∈ (𝐹𝐼𝑌)) & ⊢ (𝜑 → (𝐸 − 𝑌) = (𝐸 − 𝐶)) & ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘𝑅)‘𝑌)) & ⊢ (𝜑 → 𝑌 ∈ (𝐸𝐼𝑍)) & ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝑅)) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑅𝐼𝑄)) & ⊢ (𝜑 → (𝑌 − 𝑄) = (𝑌 − 𝐸)) & ⊢ (𝜑 → 𝑌 ∈ ((((pInvG‘𝐺)‘𝑍)‘𝑄)𝐼𝐷)) & ⊢ (𝜑 → (𝑌 − 𝐷) = (𝑌 − 𝐶)) & ⊢ (𝜑 → 𝐷 = (((pInvG‘𝐺)‘𝑋)‘𝐶)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐴) | ||
Theorem | footexlem2 28544 | Lemma for footex 28545. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 = (𝐸𝐿𝐹)) & ⊢ (𝜑 → 𝐸 ≠ 𝐹) & ⊢ (𝜑 → 𝐸 ∈ (𝐹𝐼𝑌)) & ⊢ (𝜑 → (𝐸 − 𝑌) = (𝐸 − 𝐶)) & ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘𝑅)‘𝑌)) & ⊢ (𝜑 → 𝑌 ∈ (𝐸𝐼𝑍)) & ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝑅)) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑅𝐼𝑄)) & ⊢ (𝜑 → (𝑌 − 𝑄) = (𝑌 − 𝐸)) & ⊢ (𝜑 → 𝑌 ∈ ((((pInvG‘𝐺)‘𝑍)‘𝑄)𝐼𝐷)) & ⊢ (𝜑 → (𝑌 − 𝐷) = (𝑌 − 𝐶)) & ⊢ (𝜑 → 𝐷 = (((pInvG‘𝐺)‘𝑋)‘𝐶)) ⇒ ⊢ (𝜑 → (𝐶𝐿𝑋)(⟂G‘𝐺)𝐴) | ||
Theorem | footex 28545* | From a point 𝐶 outside of a line 𝐴, there exists a point 𝑥 on 𝐴 such that (𝐶𝐿𝑥) is perpendicular to 𝐴. This point is unique, see foot 28546. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴) | ||
Theorem | foot 28546* | 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 28547 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐴) | ||
Theorem | footeq 28548 | Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴) & ⊢ (𝜑 → (𝑌𝐿𝑍)(⟂G‘𝐺)𝐴) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | hlperpnel 28549 | 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 28550 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝐷)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐶𝐷”〉 ∈ (∟G‘𝐺)) | ||
Theorem | perpdragALT 28551 | 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 28552 | Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐵𝐿𝐶)) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (∟G‘𝐺)) | ||
Theorem | colperp 28553 | Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)𝐷) & ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴𝐿𝐶)(⟂G‘𝐺)𝐷) | ||
Theorem | colperpexlem1 28554 | Lemma for colperp 28553. 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 28555 | Lemma for colperpex 28557. 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 28556* | Lemma for colperpex 28557. 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 28557* | 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 28558 | Lemma for opphllem 28559, which is itself used for mideu 28562. (Contributed by Thierry Arnoux, 19-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑂 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵)) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂)) & ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂)) & ⊢ (𝜑 → 𝑅 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄)) & ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (𝑇𝐼𝐵)) & ⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂)) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍)) & ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅)) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍)) ⇒ ⊢ (𝜑 → 𝐵 = 𝑀) | ||
Theorem | opphllem 28559* | Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 28560 and later for opphl 28578. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = (pInvG‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑂 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵)) & ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂)) & ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂)) & ⊢ (𝜑 → 𝑅 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄)) & ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝐵 = ((𝑆‘𝑥)‘𝐴) ∧ 𝑂 = ((𝑆‘𝑥)‘𝑅))) | ||
Theorem | mideulem 28560* | Lemma for mideu 28562. 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 28561* | 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 28562* | 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 28563* | 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 28564* | Deduce that 𝐴 and 𝐵 lie on opposite sides of line 𝐿. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵)) ⇒ ⊢ (𝜑 → 𝐴𝑂𝐵) | ||
Theorem | oppne1 28565* | 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 28566* | 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 28567* | 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 28568* | 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 28569* | 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 28570* | The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑂𝐴) | ||
Theorem | opphllem1 28571* | Lemma for opphl 28578. (Contributed by Thierry Arnoux, 20-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝑀 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 = (𝑆‘𝐶)) & ⊢ (𝜑 → 𝐴 ≠ 𝑅) & ⊢ (𝜑 → 𝐵 ≠ 𝑅) & ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐴)) ⇒ ⊢ (𝜑 → 𝐵𝑂𝐶) | ||
Theorem | opphllem2 28572* | Lemma for opphl 28578. Lemma 9.3 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝑀 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 = (𝑆‘𝐶)) & ⊢ (𝜑 → 𝐴 ≠ 𝑅) & ⊢ (𝜑 → 𝐵 ≠ 𝑅) & ⊢ (𝜑 → (𝐴 ∈ (𝑅𝐼𝐵) ∨ 𝐵 ∈ (𝑅𝐼𝐴))) ⇒ ⊢ (𝜑 → 𝐵𝑂𝐶) | ||
Theorem | opphllem3 28573* | Lemma for opphl 28578: 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 28574* | Lemma for opphl 28578. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ 𝑁 = ((pInvG‘𝐺)‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝐷) & ⊢ (𝜑 → 𝑀 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) & ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) & ⊢ (𝜑 → 𝑅 ≠ 𝑆) & ⊢ (𝜑 → (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → (𝑁‘𝑅) = 𝑆) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈(𝐾‘𝑅)𝐴) & ⊢ (𝜑 → 𝑉(𝐾‘𝑆)𝐶) ⇒ ⊢ (𝜑 → 𝑈𝑂𝑉) | ||
Theorem | opphllem5 28575* | 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 28576* | 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 28577* | Restating colperpex 28557 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 28578* | If two points 𝐴 and 𝐶 lie on opposite sides 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 28579* | 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 28580* | An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶)) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))) | ||
Syntax | chpg 28581 | "Belong to the same open half-plane" relation for points in a geometry. |
class hpG | ||
Definition | df-hpg 28582* | Define the open half plane relation for a geometry 𝐺. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 28584 to find the same formulation. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))})) | ||
Theorem | ishpg 28583* | 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 28584* | 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 28585* | 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 28586* | 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 28587* | Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐴𝑂𝐶) ⇒ ⊢ (𝜑 → (𝐵𝑂𝐶 ↔ 𝐴((hpG‘𝐺)‘𝐷)𝐵)) | ||
Theorem | lnoppnhpg 28588* | 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 28589* | 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 28590* | 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 28591* | 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 28592* | 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 28593* | 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 28594* | 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 28595* | 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 28596 | Declare the constant for the midpoint operation. |
class midG | ||
Syntax | clmi 28597 | Declare the constant for the line mirroring function. |
class lInvG | ||
Definition | df-mid 28598* | Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 28602, midbtwn 28603, and midcgr 28604. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
⊢ midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)))) | ||
Definition | df-lmi 28599* | Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 28611. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ lInvG = (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))) | ||
Theorem | midf 28600 | Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐺DimTarskiG≥2) ⇒ ⊢ (𝜑 → (midG‘𝐺):(𝑃 × 𝑃)⟶𝑃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |