P. 285 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28401-28500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tgbtwnconn22 28401	Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐸))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐷𝐼𝐸))
Theorem	tgbtwnconnln1 28402	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))
Theorem	tgbtwnconnln2 28403	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 28404	Less-than relation for geometric congruences.
class ≤G
Definition	df-leg 28405*	Define the less-than relationship between geometric distance congruence classes. See legval 28406. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ ≤G = (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})
Theorem	legval 28406*	Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ≤ = {⟨𝑒, 𝑓⟩ ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))})
Theorem	legov 28407*	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 28408*	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 28409	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 28410	Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐶))
Theorem	legtrd 28411	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 28412	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 28413	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 28414	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 28415	Deduce equality from "less than" null segments. (Contributed by Thierry Arnoux, 12-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	legbtwn 28416	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 28417	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 28418*	The set 𝐸 denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝐴 = (𝑥 − 𝑦))
Theorem	ltgov 28419	Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ < = (( ≤ ↾ 𝐸) ∖ I )    &   ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷))))
Theorem	legov3 28420	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 28421	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 28422	Function producing the relation "belong to the same half-line".
class hlG
Definition	df-hlg 28423*	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 28424	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 28425	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐵(𝐾‘𝐶)𝐴))
Theorem	hlcomd 28426	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵(𝐾‘𝐶)𝐴)
Theorem	hlne1 28427	The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	hlne2 28428	The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	hlln 28429	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 28430	The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝐵)
Theorem	hlid 28431	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 28432	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 28433	Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶𝐼𝐵))    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐴(𝐾‘𝐶)𝐷))
Theorem	btwnhl1 28434	Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶(𝐾‘𝐴)𝐵)
Theorem	btwnhl2 28435	Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐵))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐴)
Theorem	btwnhl 28436	Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐼𝐶))
Theorem	lnhl 28437	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 28438*	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 28439	Lemma for hlcgreu 28440. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋(𝐾‘𝐴)𝐷)    &   ⊢ (𝜑 → 𝑌(𝐾‘𝐴)𝐷)    &   ⊢ (𝜑 → (𝐴 − 𝑋) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐴 − 𝑌) = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	hlcgreu 28440*	The point constructed in hlcgrex 28438 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 28441	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	btwnlng2 28442	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	btwnlng3 28443	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	lncom 28444	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 28445	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 28446	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 28447	Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)
Theorem	ncolne2 28448	Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) TODO (NM): maybe ncolne2 28448 could be simplified out and deleted, replaced by ncolcom 28383.
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑍)
Theorem	tgisline 28449*	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 28450	It takes two different points to form a line. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)
Theorem	tglndim0 28451	There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ ran 𝐿)
Theorem	tgelrnln 28452	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 28453	Transitivity law for lines, one half of tglineelsb2 28454. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑄)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ≠ 𝑃)    &   ⊢ (𝜑 → 𝑆 ∈ (𝑃𝐿𝑄))    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑆))    ⇒   ⊢ (𝜑 → 𝑅 ∈ (𝑃𝐿𝑄))
Theorem	tglineelsb2 28454	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 28455	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 28456	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 28457	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 28458	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 28459*	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 28460*	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 28461*	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 28462	A line 𝐴 has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	tglnpt2 28463*	Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦)
Theorem	tglineintmo 28464*	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 28465	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 28466	Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))    ⇒   ⊢ (𝜑 → (𝐴𝐿𝐵) ≠ (𝐶𝐿𝐷))
Theorem	tglineinteq 28467	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 28468	Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐿𝐵))    &   ⊢ (𝜑 → 𝐷 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
Theorem	coltr 28469	A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶))    &   ⊢ (𝜑 → (𝐵 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))
Theorem	coltr3 28470	A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝐵𝐿𝐶))
Theorem	colline 28471*	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 28472*	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 28473*	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 28474	Declare the constant for the point inversion function.
class pInvG
Definition	df-mir 28475*	Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 28477 and ismir 28481. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
Theorem	mirreu3 28476*	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 28477*	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 28478*	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 28479	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 28480	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 28481	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 28482	Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    ⇒   ⊢ (𝜑 → 𝑀:𝑃⟶𝑃)
Theorem	mircl 28483	Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃)
Theorem	mirmir 28484	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 28485	Variation on mirmir 28484. (Contributed by Thierry Arnoux, 10-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝑀‘𝐶) = 𝐵)
Theorem	mirreu 28486*	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 28487	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 28488	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 28489	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 28490	The center point is invariant of a point inversion. (Contributed by Thierry Arnoux, 25-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) = 𝐴)
Theorem	mirf1o 28491	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 28492	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 28493	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 28494	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 28495	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 28496	Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑀‘((𝑆‘𝑌)‘𝑋)) = ((𝑆‘(𝑀‘𝑌))‘(𝑀‘𝑋)))
Theorem	mirmot 28497	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 28498	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 28499	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 28500	Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝑆 = (pInvG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑀 = (𝑆‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼𝑋)))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌)))