P. 290 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28901-29000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	colline 28901*	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 28902*	Reformulation of the lower dimension axiom for dimension two. There exist three non-colinear points. Theorem 6.24 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺DimTarskiG≥2)    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ¬ (𝑐 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
Theorem	tglowdim2ln 28903*	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)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 ¬ 𝑐 ∈ (𝐴𝐿𝐵))
Theorem	tglnpt2 28904*	Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦)
Theorem	tglnpt3 28905*	Find a third point on a line. (Contributed by Thierry Arnoux, 17-Jun-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌))
Theorem	tglnpt4 28906*	Find a second point on a line, outside of a second line. (Contributed by Thierry Arnoux, 17-Jun-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ (𝐴 ∖ 𝐵)𝑧 ≠ 𝑋)
16.2.12  Point inversions
Syntax	cmir 28907	Declare the constant for the point inversion function.
class pInvG
Definition	df-mir 28908*	Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 28910 and ismir 28914. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
Theorem	mirreu3 28909*	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 28910*	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 28911*	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 28912	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 28913	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 28914	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 28915	Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    ⇒   ⊢ (𝜑 → 𝑀:𝑃⟶𝑃)
Theorem	mircl 28916	Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃)
Theorem	mirmir 28917	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 28918	Variation on mirmir 28917. (Contributed by Thierry Arnoux, 10-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝑀‘𝐶) = 𝐵)
Theorem	mirreu 28919*	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 28920	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 28921	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 28922	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 28923	The center point is invariant of a point inversion. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) = 𝐴)
Theorem	mirf1o 28924	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 28925	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 28926	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 28927	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 28928	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 28929	Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑀‘((𝑆‘𝑌)‘𝑋)) = ((𝑆‘(𝑀‘𝑌))‘(𝑀‘𝑋)))
Theorem	mirmot 28930	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 28931	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 28932	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 28933	Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼𝑋)))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌)))
Theorem	mirhl 28934	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 28935	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 28936	Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝐴)    &   ⊢ (𝜑 → 𝑌 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌)))    ⇒   ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝑌)
Theorem	mircgrextend 28937	Link congruence over a pair of mirror points. cf tgcgrextend 28732. (Contributed by Thierry Arnoux, 4-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ 𝑀 = (𝑆‘𝐵)    &   ⊢ 𝑁 = (𝑆‘𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝑋 − 𝑌))    ⇒   ⊢ (𝜑 → (𝐴 − (𝑀‘𝐴)) = (𝑋 − (𝑁‘𝑋)))
Theorem	mirtrcgr 28938	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 28939	Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝑇)    &   ⊢ 𝑋 = (𝑀‘𝐴)    &   ⊢ 𝑌 = (𝑀‘𝐵)    &   ⊢ 𝑍 = (𝑀‘𝐶)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 𝑍)
Theorem	miduniq 28940	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 28941	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 28942	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 28943	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 28944	Lemma of the symmetrical 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 28945	Lemma for krippen 28946. 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 28946	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 28947*	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 28997 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝑥)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
Theorem	symquadprlnglem 28948	Lemma for symquadprlnglem 28948. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑊))    &   ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑊 − 𝑋))    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    &   ⊢ (𝜑 → 𝑌 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑋𝐿𝑍))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑌𝐿𝑊))    ⇒   ⊢ (𝜑 → ¬ (𝑊 ∈ (𝑍𝐿𝑌) ∨ 𝑍 = 𝑌))
Theorem	mirleqb 28949	Equality theorem for point mirroring. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑋 = 𝑌 ↔ (𝑀‘𝑋) = (𝑀‘𝑌)))
Theorem	mirlni 28950	The mirror of a point 𝑋 on a line (𝑌𝐿𝑍) is on the mirrored line ((𝑀‘𝑌)𝐿(𝑀‘𝑍)). (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ ((𝑀‘𝑌)𝐿(𝑀‘𝑍)))
16.2.13  Right angles
Syntax	crag 28951	Declare the constant for the class of right angles.
class ∟G
Definition	df-rag 28952*	Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 28955. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
Syntax	cperpg 28953	Declare the constant for the perpendicular relation.
class ⟂G
Definition	df-perpg 28954*	Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 28970. (Contributed by Thierry Arnoux, 8-Sep-2019.)
⊢ ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})
Theorem	israg 28955	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 28956	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 28957	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 28958	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 28959	Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))    &   ⊢ 𝑀 = (𝑆‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ⟨“(𝑀‘𝐴)(𝑀‘𝐵)(𝑀‘𝐶)”⟩ ∈ (∟G‘𝐺))
Theorem	ragtrivb 28960	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 28961	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 28962	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 28963	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 28964	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 28965	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 28966	Right angles are preserved by motions. (Contributed by Thierry Arnoux, 16-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))    ⇒   ⊢ (𝜑 → ⟨“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”⟩ ∈ (∟G‘𝐺))
Theorem	ragncol 28967	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 28968	Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
Theorem	perpln2 28969	Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)
Theorem	isperp 28970*	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 28971	The "perpendicular" relation is symmetric. 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 28972	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 28973*	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 28974	One direction of isperp2 28973. (Contributed by Thierry Arnoux, 10-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝑈𝑋𝑉”⟩ ∈ (∟G‘𝐺))
Theorem	ragperp 28975	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 28976*	Alternative version of footex 28979 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 28977	Lemma for footex 28979. (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 28978	Lemma for footex 28979. (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 28979*	From a point 𝐶 outside of a line 𝐴, there exists a point 𝑥 on 𝐴 such that (𝐶𝐿𝑥) is perpendicular to 𝐴. This point is unique, see foot 28980. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
Theorem	foot 28980*	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 28981	Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐴)
Theorem	footeq 28982	Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴)    &   ⊢ (𝜑 → (𝑌𝐿𝑍)(⟂G‘𝐺)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	perpin 28983	If two lines 𝐴 and 𝐵 are perpendicular, then they intersect. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅)
Theorem	hlperpnel 28984	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 28985	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝐷))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐶𝐷”⟩ ∈ (∟G‘𝐺))
Theorem	perpdragALT 28986	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 28987	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐵𝐿𝐶))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))
Theorem	colperp 28988	Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)𝐷)    &   ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴𝐿𝐶)(⟂G‘𝐺)𝐷)
Theorem	colperpexlem1 28989	Lemma for colperp 28988. 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 28990	Lemma for colperpex 28992. 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 28991*	Lemma for colperpex 28992. 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 28992*	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 28993	Lemma for opphllem 28994, which is itself used for mideu 28997. (Contributed by Thierry Arnoux, 19-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))    &   ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))    &   ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑇𝐼𝐵))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))    &   ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍))    ⇒   ⊢ (𝜑 → 𝐵 = 𝑀)
Theorem	opphllem 28994*	Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 28995 and later for opphl 29013. (Contributed by Thierry Arnoux, 21-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))    &   ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))    &   ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝐵 = ((𝑆‘𝑥)‘𝐴) ∧ 𝑂 = ((𝑆‘𝑥)‘𝑅)))
Theorem	mideulem 28995*	Lemma for mideu 28997. 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 28996*	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 28997*	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)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑃 𝐵 = ((𝑆‘𝑥)‘𝐴))
16.2.14  Half-planes
Theorem	islnopp 28998*	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 28999*	Deduce that 𝐴 and 𝐵 lie on opposite sides of line 𝐿. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵))    ⇒   ⊢ (𝜑 → 𝐴𝑂𝐵)
Theorem	oppne1 29000*	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)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷)