P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tglowdim2l 29101*	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 29102*	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 29103*	Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦)
Theorem	tglnpt3 29104*	Find a third point on a line. (Contributed by Thierry Arnoux, 17-Jun-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑌))
Theorem	tglnpt4 29105*	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 29106	Declare the constant for the point inversion function.
class pInvG
Definition	df-mir 29107*	Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 29109 and ismir 29113. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
Theorem	mirreu3 29108*	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 29109*	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 29110*	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 29111	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 29112	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 29113	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 29114	Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    ⇒   ⊢ (𝜑 → 𝑀:𝑃⟶𝑃)
Theorem	mircl 29115	Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃)
Theorem	mirmir 29116	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 29117	Variation on mirmir 29116. (Contributed by Thierry Arnoux, 10-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝑀‘𝐶) = 𝐵)
Theorem	mirreu 29118*	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 29119	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 29120	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 29121	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 29122	The center point is invariant of a point inversion. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) = 𝐴)
Theorem	mirf1o 29123	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 29124	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 29125	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 29126	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 29127	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 29128	Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑀‘((𝑆‘𝑌)‘𝑋)) = ((𝑆‘(𝑀‘𝑌))‘(𝑀‘𝑋)))
Theorem	mirmot 29129	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 29130	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 29131	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 29132	Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼𝑋)))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌)))
Theorem	mirhl 29133	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 29134	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 29135	Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝐴)    &   ⊢ (𝜑 → 𝑌 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌)))    ⇒   ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝑌)
Theorem	mircgrextend 29136	Link congruence over a pair of mirror points. cf tgcgrextend 28929. (Contributed by Thierry Arnoux, 4-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ 𝑀 = (𝑆‘𝐵)    &   ⊢ 𝑁 = (𝑆‘𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝑋 − 𝑌))    ⇒   ⊢ (𝜑 → (𝐴 − (𝑀‘𝐴)) = (𝑋 − (𝑁‘𝑋)))
Theorem	mirtrcgr 29137	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 29138	Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝑇)    &   ⊢ 𝑋 = (𝑀‘𝐴)    &   ⊢ 𝑌 = (𝑀‘𝐵)    &   ⊢ 𝑍 = (𝑀‘𝐶)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 𝑍)
Theorem	miduniq 29139	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 29140	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 29141	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 29142	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 29143	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 29144	Lemma for krippen 29145. 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 29145	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 29146*	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 29196 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝑥)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
Theorem	symquadprlnglem 29147	Lemma for symquadprlnglem 29147. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑊))    &   ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑊 − 𝑋))    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    &   ⊢ (𝜑 → 𝑌 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑋𝐿𝑍))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑌𝐿𝑊))    ⇒   ⊢ (𝜑 → ¬ (𝑊 ∈ (𝑍𝐿𝑌) ∨ 𝑍 = 𝑌))
Theorem	mirleqb 29148	Equality theorem for point mirroring. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑋 = 𝑌 ↔ (𝑀‘𝑋) = (𝑀‘𝑌)))
Theorem	mirlni 29149	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 29150	Declare the constant for the class of right angles.
class ∟G
Definition	df-rag 29151*	Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 29154. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
Syntax	cperpg 29152	Declare the constant for the perpendicular relation.
class ⟂G
Definition	df-perpg 29153*	Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 29169. (Contributed by Thierry Arnoux, 8-Sep-2019.)
⊢ ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})
Theorem	israg 29154	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 29155	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 29156	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 29157	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 29158	Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))    &   ⊢ 𝑀 = (𝑆‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ⟨“(𝑀‘𝐴)(𝑀‘𝐵)(𝑀‘𝐶)”⟩ ∈ (∟G‘𝐺))
Theorem	ragtrivb 29159	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 29160	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 29161	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 29162	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 29163	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 29164	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 29165	Right angles are preserved by motions. (Contributed by Thierry Arnoux, 16-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))    ⇒   ⊢ (𝜑 → ⟨“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”⟩ ∈ (∟G‘𝐺))
Theorem	ragncol 29166	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 29167	Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
Theorem	perpln2 29168	Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)
Theorem	isperp 29169*	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 29170	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 29171	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 29172*	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 29173	One direction of isperp2 29172. (Contributed by Thierry Arnoux, 10-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝑈𝑋𝑉”⟩ ∈ (∟G‘𝐺))
Theorem	ragperp 29174	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 29175*	Alternative version of footex 29178 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 29176	Lemma for footex 29178. (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 29177	Lemma for footex 29178. (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 29178*	From a point 𝐶 outside of a line 𝐴, there exists a point 𝑥 on 𝐴 such that (𝐶𝐿𝑥) is perpendicular to 𝐴. This point is unique, see foot 29179. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
Theorem	foot 29179*	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 29180	Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐴)
Theorem	footeq 29181	Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴)    &   ⊢ (𝜑 → (𝑌𝐿𝑍)(⟂G‘𝐺)𝐴)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	perpin 29182	If two lines 𝐴 and 𝐵 are perpendicular, then they intersect. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅)
Theorem	hlperpnel 29183	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 29184	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝐷))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐶𝐷”⟩ ∈ (∟G‘𝐺))
Theorem	perpdragALT 29185	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 29186	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐵𝐿𝐶))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))
Theorem	colperp 29187	Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)𝐷)    &   ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴𝐿𝐶)(⟂G‘𝐺)𝐷)
Theorem	colperpexlem1 29188	Lemma for colperp 29187. 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 29189	Lemma for colperpex 29191. 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 29190*	Lemma for colperpex 29191. 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 29191*	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 29192	Lemma for opphllem 29193, which is itself used for mideu 29196. (Contributed by Thierry Arnoux, 19-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))    &   ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))    &   ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑇𝐼𝐵))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))    &   ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍))    ⇒   ⊢ (𝜑 → 𝐵 = 𝑀)
Theorem	opphllem 29193*	Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 29194 and later for opphl 29212. (Contributed by Thierry Arnoux, 21-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))    &   ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))    &   ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))    &   ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝐵 = ((𝑆‘𝑥)‘𝐴) ∧ 𝑂 = ((𝑆‘𝑥)‘𝑅)))
Theorem	mideulem 29194*	Lemma for mideu 29196. 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 29195*	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 29196*	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 29197*	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 29198*	Deduce that 𝐴 and 𝐵 lie on opposite sides of line 𝐿. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵))    ⇒   ⊢ (𝜑 → 𝐴𝑂𝐵)
Theorem	oppne1 29199*	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 29200*	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)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷)