P. 279 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27801-27900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ncolcom 27801	Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋))
Theorem	ncolrot1 27802	Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))
Theorem	ncolrot2 27803	Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → ¬ (𝑌 ∈ (𝑍𝐿𝑋) ∨ 𝑍 = 𝑋))
Theorem	tgdim01ln 27804	In geometries of dimension less than two, then any three points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ 𝐺DimTarskiG≥2)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
Theorem	ncoltgdim2 27805	If there are three non-colinear points, then the dimension is at least two. Converse of tglowdim2l 27890. (Contributed by Thierry Arnoux, 23-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → 𝐺DimTarskiG≥2)
Theorem	lnxfr 27806	Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
Theorem	lnext 27807*	Extend a line with a missing point. Theorem 4.14 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))    &   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝑐”⟩)
Theorem	tgfscgr 27808	Congruence law for the general five segment configuration. Theorem 4.16 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)    &   ⊢ (𝜑 → (𝑋 − 𝑇) = (𝐴 − 𝐷))    &   ⊢ (𝜑 → (𝑌 − 𝑇) = (𝐵 − 𝐷))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    ⇒   ⊢ (𝜑 → (𝑍 − 𝑇) = (𝐶 − 𝐷))
Theorem	lncgr 27809	Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 28-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))    &   ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑋 − 𝐵))    &   ⊢ (𝜑 → (𝑌 − 𝐴) = (𝑌 − 𝐵))    ⇒   ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − 𝐵))
Theorem	lnid 27810	Identity law for points on lines. Theorem 4.18 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍))    &   ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝐴))    &   ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝐴))    ⇒   ⊢ (𝜑 → 𝑍 = 𝐴)
Theorem	tgidinside 27811	Law for finding a point inside a segment. Theorem 4.19 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌))    &   ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝐴))    &   ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝐴))    ⇒   ⊢ (𝜑 → 𝑍 = 𝐴)
16.2.8  Connectivity of betweenness
Theorem	tgbtwnconn1lem1 27812	Lemma for tgbtwnconn1 27815. (Contributed by Thierry Arnoux, 30-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽))    &   ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷))    ⇒   ⊢ (𝜑 → 𝐻 = 𝐽)
Theorem	tgbtwnconn1lem2 27813	Lemma for tgbtwnconn1 27815. (Contributed by Thierry Arnoux, 30-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽))    &   ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐸 − 𝐹) = (𝐶 − 𝐷))
Theorem	tgbtwnconn1lem3 27814	Lemma for tgbtwnconn1 27815. (Contributed by Thierry Arnoux, 30-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽))    &   ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐼𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐷𝐼𝐹))    &   ⊢ (𝜑 → 𝐶 ≠ 𝐸)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐹)
Theorem	tgbtwnconn1 27815	Connectivity law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶)))
Theorem	tgbtwnconn2 27816	Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
Theorem	tgbtwnconn3 27817	Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵)))
Theorem	tgbtwnconnln3 27818	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))    &   ⊢ 𝐿 = (LineG‘𝐺)    ⇒   ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
Theorem	tgbtwnconn22 27819	Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐸))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐷𝐼𝐸))
Theorem	tgbtwnconnln1 27820	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))
Theorem	tgbtwnconnln2 27821	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))
16.2.9  Less-than relation in geometric congruences
Syntax	cleg 27822	Less-than relation for geometric congruences.
class ≤G
Definition	df-leg 27823*	Define the less-than relationship between geometric distance congruence classes. See legval 27824. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ ≤G = (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})
Theorem	legval 27824*	Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ≤ = {⟨𝑒, 𝑓⟩ ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))})
Theorem	legov 27825*	Value of the less-than relationship. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑧))))
Theorem	legov2 27826*	An equivalent definition of the less-than relationship. Definition 5.5 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑥 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐶 − 𝐷))))
Theorem	legid 27827	Reflexivity of the less-than relationship. Proposition 5.7 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐵))
Theorem	btwnleg 27828	Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐶))
Theorem	legtrd 27829	Transitivity of the less-than relationship. Proposition 5.8 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐸 − 𝐹))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐸 − 𝐹))
Theorem	legtri3 27830	Equality from the less-than relationship. Proposition 5.9 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐴 − 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))
Theorem	legtrid 27831	Trichotomy law for the less-than relationship. Proposition 5.10 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∨ (𝐶 − 𝐷) ≤ (𝐴 − 𝐵)))
Theorem	leg0 27832	Degenerated (zero-length) segments are minimal. Proposition 5.11 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐴) ≤ (𝐶 − 𝐷))
Theorem	legeq 27833	Deduce equality from "less than" null segments. (Contributed by Thierry Arnoux, 12-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	legbtwn 27834	Deduce betweenness from "less than" relation. Corresponds loosely to Proposition 6.13 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))    &   ⊢ (𝜑 → (𝐶 − 𝐴) ≤ (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐶𝐼𝐵))
Theorem	tgcgrsub2 27835	Removing identical parts from the end of a line segment preserves congruence. In this version the order of points is not known. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵)))    &   ⊢ (𝜑 → (𝐸 ∈ (𝐷𝐼𝐹) ∨ 𝐹 ∈ (𝐷𝐼𝐸)))    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))
Theorem	ltgseg 27836*	The set 𝐸 denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝐴 = (𝑥 − 𝑦))
Theorem	ltgov 27837	Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ < = (( ≤ ↾ 𝐸) ∖ I )    &   ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷))))
Theorem	legov3 27838	An equivalent definition of the less-than relationship, from the strict relation. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ < = (( ≤ ↾ 𝐸) ∖ I )    &   ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) < (𝐶 − 𝐷) ∨ (𝐴 − 𝐵) = (𝐶 − 𝐷))))
Theorem	legso 27839	The "shorter than" relation induces an order on pairs. Remark 5.13 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ < = (( ≤ ↾ 𝐸) ∖ I )    &   ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − )    ⇒   ⊢ (𝜑 → < Or 𝐸)
16.2.10  Rays
Syntax	chlg 27840	Function producing the relation "belong to the same half-line".
class hlG
Definition	df-hlg 27841*	Define the function producting the relation "belong to the same half-line". (Contributed by Thierry Arnoux, 15-Aug-2020.)
⊢ hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}))
Theorem	ishlg 27842	Rays : Definition 6.1 of [Schwabhauser] p. 43. With this definition, 𝐴(𝐾‘𝐶)𝐵 means that 𝐴 and 𝐵 are on the same ray with initial point 𝐶. This follows the same notation as Schwabhauser where rays are first defined as a relation. It is possible to recover the ray itself using e.g., ((𝐾‘𝐶) “ {𝐴}). (Contributed by Thierry Arnoux, 21-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
Theorem	hlcomb 27843	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐵(𝐾‘𝐶)𝐴))
Theorem	hlcomd 27844	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵(𝐾‘𝐶)𝐴)
Theorem	hlne1 27845	The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	hlne2 27846	The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	hlln 27847	The half-line relation implies colinearity, part of Theorem 6.4 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 22-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶))
Theorem	hleqnid 27848	The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝐵)
Theorem	hlid 27849	The half-line relation is reflexive. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐴)
Theorem	hltr 27850	The half-line relation is transitive. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 23-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵)    &   ⊢ (𝜑 → 𝐵(𝐾‘𝐷)𝐶)    ⇒   ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐶)
Theorem	hlbtwn 27851	Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶𝐼𝐵))    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐴(𝐾‘𝐶)𝐷))
Theorem	btwnhl1 27852	Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶(𝐾‘𝐴)𝐵)
Theorem	btwnhl2 27853	Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐴)
Theorem	btwnhl 27854	Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐼𝐶))
Theorem	lnhl 27855	Either a point 𝐶 on the line AB is on the same side as 𝐴 or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵))    ⇒   ⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐴 ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
Theorem	hlcgrex 27856*	Construct a point on a half-line, at a given distance of its origin. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥(𝐾‘𝐴)𝐷 ∧ (𝐴 − 𝑥) = (𝐵 − 𝐶)))
Theorem	hlcgreulem 27857	Lemma for hlcgreu 27858. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝐷)    &   ⊢ (𝜑 → 𝑌(𝐾‘𝐴)𝐷)    &   ⊢ (𝜑 → (𝐴 − 𝑋) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐴 − 𝑌) = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	hlcgreu 27858*	The point constructed in hlcgrex 27856 is unique. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑃 (𝑥(𝐾‘𝐴)𝐷 ∧ (𝐴 − 𝑥) = (𝐵 − 𝐶)))
16.2.11  Lines
Theorem	btwnlng1 27859	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	btwnlng2 27860	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	btwnlng3 27861	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	lncom 27862	Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑌𝐿𝑋))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	lnrot1 27863	Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐿𝑋))    &   ⊢ (𝜑 → 𝑍 ≠ 𝑋)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	lnrot2 27864	Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍))    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	ncolne1 27865	Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)
Theorem	ncolne2 27866	Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) TODO (NM): maybe ncolne2 27866 could be simplified out and deleted, replaced by ncolcom 27801.
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑍)
Theorem	tgisline 27867*	The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝐴 = (𝑥𝐿𝑦) ∧ 𝑥 ≠ 𝑦))
Theorem	tglnne 27868	It takes two different points to form a line. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)
Theorem	tglndim0 27869	There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ ran 𝐿)
Theorem	tgelrnln 27870	The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    ⇒   ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
Theorem	tglineeltr 27871	Transitivity law for lines, one half of tglineelsb2 27872. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ≠ 𝑃)    &   ⊢ (𝜑 → 𝑆 ∈ (𝑃𝐿𝑄))    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑆))    ⇒   ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑄))
Theorem	tglineelsb2 27872	If 𝑆 lies on PQ , then PQ = PS . Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ≠ 𝑃)    &   ⊢ (𝜑 → 𝑆 ∈ (𝑃𝐿𝑄))    ⇒   ⊢ (𝜑 → (𝑃𝐿𝑄) = (𝑃𝐿𝑆))
Theorem	tglinerflx1 27873	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝑃𝐿𝑄))
Theorem	tglinerflx2 27874	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → 𝑄 ∈ (𝑃𝐿𝑄))
Theorem	tglinecom 27875	Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → (𝑃𝐿𝑄) = (𝑄𝐿𝑃))
Theorem	tglinethru 27876	If 𝐴 is a line containing two distinct points 𝑃 and 𝑄, then 𝐴 is the line through 𝑃 and 𝑄. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = (𝑃𝐿𝑄))
Theorem	tghilberti1 27877*	There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ran 𝐿(𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	tghilberti2 27878*	There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → ∃*𝑥 ∈ ran 𝐿(𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	tglinethrueu 27879*	There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ran 𝐿(𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	tglnne0 27880	A line 𝐴 has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	tglnpt2 27881*	Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦)
Theorem	tglineintmo 27882*	Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	tglineineq 27883	Two distinct lines intersect in at most one point, variation. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	tglineneq 27884	Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))    ⇒   ⊢ (𝜑 → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷))
Theorem	tglineinteq 27885	Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐿𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐿𝐷))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	ncolncol 27886	Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝐷 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
Theorem	coltr 27887	A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶))    &   ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))
Theorem	coltr3 27888	A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐿𝐶))
Theorem	colline 27889*	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 27890*	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 27891*	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)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 ¬ 𝑐 ∈ (𝐴𝐿𝐵))
16.2.12  Point inversions
Syntax	cmir 27892	Declare the constant for the point inversion function.
class pInvG
Definition	df-mir 27893*	Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 27895 and ismir 27899. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
Theorem	mirreu3 27894*	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 27895*	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 27896*	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 27897	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 27898	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 27899	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 27900	Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    ⇒   ⊢ (𝜑 → 𝑀:𝑃⟶𝑃)