P. 284 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28301-28400   *Has distinct variable group(s)

Type	Label	Description
Statement
16.2.5  Congruence of a series of points
Syntax	ccgrg 28301	Declare the constant for the congruence between shapes relation.
class cgrG
Definition	df-cgrg 28302*	Define the relation of congruence between shapes. Definition 4.4 of [Schwabhauser] p. 35. A "shape" is a finite sequence of points, and a triangle can be represented as a shape with three points. Two shapes are congruent if all corresponding segments between all corresponding points are congruent. Many systems of geometry define triangle congruence as requiring both segment congruence and angle congruence. Such systems, such as Hilbert's axiomatic system, typically have a primitive notion of angle congruence in addition to segment congruence. Here, angle congruence is instead a derived notion, defined later in df-cgra 28599 and expanded in iscgra 28600. This does not mean our system is weaker; dfcgrg2 28654 proves that these two definitions are equivalent, and using the Tarski definition instead (given in [Schwabhauser] p. 35) is simpler. Once two triangles are proven congruent as defined here, you can use various theorems to prove that corresponding parts of congruent triangles are congruent (CPCTC). For example, see cgr3simp1 28311, cgr3simp2 28312, cgr3simp3 28313, cgrcgra 28612, and permutation laws such as cgr3swap12 28314 and dfcgrg2 28654. Ideally, we would define this for functions of any set, but we will use words (see df-word 14489) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})
Theorem	iscgrg 28303*	The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))))
Theorem	iscgrgd 28304*	The property for two sequences 𝐴 and 𝐵 of points to be congruent. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴:𝐷⟶𝑃)    &   ⊢ (𝜑 → 𝐵:𝐷⟶𝑃)    ⇒   ⊢ (𝜑 → (𝐴 ∼ 𝐵 ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))
Theorem	iscgrglt 28305*	The property for two sequences 𝐴 and 𝐵 of points to be congruent, where the congruence is only required for indices verifying a less-than relation. (Contributed by Thierry Arnoux, 7-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴:𝐷⟶𝑃)    &   ⊢ (𝜑 → 𝐵:𝐷⟶𝑃)    ⇒   ⊢ (𝜑 → (𝐴 ∼ 𝐵 ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴(𝑖 < 𝑗 → ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
Theorem	trgcgrg 28306	The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷))))
Theorem	trgcgr 28307	Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
Theorem	ercgrg 28308	The shape congruence relation is an equivalence relation. Statement 4.4 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiG → (cgrG‘𝐺) Er (𝑃 ↑pm ℝ))
Theorem	tgcgrxfr 28309*	A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹))    ⇒   ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩))
Theorem	cgr3id 28310	Reflexivity law for three-place congruence. (Contributed by Thierry Arnoux, 28-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
Theorem	cgr3simp1 28311	Deduce segment congruence from a triangle congruence. This is a portion of the theorem that corresponding parts of congruent triangles are congruent (CPCTC), focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))
Theorem	cgr3simp2 28312	Deduce segment congruence from a triangle congruence. This is a portion of CPCTC, focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))
Theorem	cgr3simp3 28313	Deduce segment congruence from a triangle congruence. This is a portion of CPCTC, focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))
Theorem	cgr3swap12 28314	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐵𝐴𝐶”⟩ ∼ ⟨“𝐸𝐷𝐹”⟩)
Theorem	cgr3swap23 28315	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐶𝐵”⟩ ∼ ⟨“𝐷𝐹𝐸”⟩)
Theorem	cgr3swap13 28316	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 3-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐶𝐵𝐴”⟩ ∼ ⟨“𝐹𝐸𝐷”⟩)
Theorem	cgr3rotr 28317	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐶𝐴𝐵”⟩ ∼ ⟨“𝐹𝐷𝐸”⟩)
Theorem	cgr3rotl 28318	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐵𝐶𝐴”⟩ ∼ ⟨“𝐸𝐹𝐷”⟩)
Theorem	trgcgrcom 28319	Commutative law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
Theorem	cgr3tr 28320	Transitivity law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩ ∼ ⟨“𝐽𝐾𝐿”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐽𝐾𝐿”⟩)
Theorem	tgbtwnxfr 28321	A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of [Schwabhauser] p. 36. (Contributed by Thierry Arnoux, 27-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))
Theorem	tgcgr4 28322	Two quadrilaterals to be congruent to each other if one triangle formed by their vertices is, and the additional points are equidistant too. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶𝐷”⟩ ∼ ⟨“𝑊𝑋𝑌𝑍”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝑊𝑋𝑌”⟩ ∧ ((𝐴 − 𝐷) = (𝑊 − 𝑍) ∧ (𝐵 − 𝐷) = (𝑋 − 𝑍) ∧ (𝐶 − 𝐷) = (𝑌 − 𝑍)))))
16.2.6  Motions
Syntax	cismt 28323	Declare the constant for the isometry builder.
class Ismt
Definition	df-ismt 28324*	Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 28325. (Contributed by Thierry Arnoux, 13-Dec-2019.)
⊢ Ismt = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑔)–1-1-onto→(Base‘ℎ) ∧ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)((𝑓‘𝑎)(dist‘ℎ)(𝑓‘𝑏)) = (𝑎(dist‘𝑔)𝑏))})
Theorem	isismt 28325*	Property of being an isometry. Compare with isismty 37209. (Contributed by Thierry Arnoux, 13-Dec-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ − = (dist‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → (𝐹 ∈ (𝐺Ismt𝐻) ↔ (𝐹:𝐵–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎𝐷𝑏))))
Theorem	ismot 28326*	Property of being an isometry mapping to the same space. In geometry, this is also called a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → (𝐹 ∈ (𝐺Ismt𝐺) ↔ (𝐹:𝑃–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((𝐹‘𝑎) − (𝐹‘𝑏)) = (𝑎 − 𝑏))))
Theorem	motcgr 28327	Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐵)) = (𝐴 − 𝐵))
Theorem	idmot 28328	The identity is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( I ↾ 𝑃) ∈ (𝐺Ismt𝐺))
Theorem	motf1o 28329	Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    ⇒   ⊢ (𝜑 → 𝐹:𝑃–1-1-onto→𝑃)
Theorem	motcl 28330	Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑃)
Theorem	motco 28331	The composition of two motions is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐺Ismt𝐺))
Theorem	cnvmot 28332	The converse of a motion is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    ⇒   ⊢ (𝜑 → ◡𝐹 ∈ (𝐺Ismt𝐺))
Theorem	motplusg 28333*	The operation for motions is their composition. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ 𝐼 = {⟨(Base‘ndx), (𝐺Ismt𝐺)⟩, ⟨(+g‘ndx), (𝑓 ∈ (𝐺Ismt𝐺), 𝑔 ∈ (𝐺Ismt𝐺) ↦ (𝑓 ∘ 𝑔))⟩}    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺))    ⇒   ⊢ (𝜑 → (𝐹(+g‘𝐼)𝐻) = (𝐹 ∘ 𝐻))
Theorem	motgrp 28334*	The motions of a geometry form a group with respect to function composition, called the Isometry group. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ 𝐼 = {⟨(Base‘ndx), (𝐺Ismt𝐺)⟩, ⟨(+g‘ndx), (𝑓 ∈ (𝐺Ismt𝐺), 𝑔 ∈ (𝐺Ismt𝐺) ↦ (𝑓 ∘ 𝑔))⟩}    ⇒   ⊢ (𝜑 → 𝐼 ∈ Grp)
Theorem	motcgrg 28335*	Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ 𝐼 = {⟨(Base‘ndx), (𝐺Ismt𝐺)⟩, ⟨(+g‘ndx), (𝑓 ∈ (𝐺Ismt𝐺), 𝑔 ∈ (𝐺Ismt𝐺) ↦ (𝑓 ∘ 𝑔))⟩}    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ Word 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝑇) ∼ 𝑇)
Theorem	motcgr3 28336	Property of a motion: distances are preserved, special case of triangles. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 = (𝐻‘𝐴))    &   ⊢ (𝜑 → 𝐸 = (𝐻‘𝐵))    &   ⊢ (𝜑 → 𝐹 = (𝐻‘𝐶))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐺Ismt𝐺))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
16.2.7  Colinearity
Theorem	tglng 28337*	Lines of a Tarski Geometry. This relates to both Definition 4.10 of [Schwabhauser] p. 36. and Definition 6.14 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiG → 𝐿 = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}))
Theorem	tglnfn 28338	Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiG → 𝐿 Fn ((𝑃 × 𝑃) ∖ I ))
Theorem	tglnunirn 28339	Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃)
Theorem	tglnpt 28340	Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑃)
Theorem	tglngne 28341	It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)
Theorem	tglngval 28342*	The line going through points 𝑋 and 𝑌. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    ⇒   ⊢ (𝜑 → (𝑋𝐿𝑌) = {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))})
Theorem	tglnssp 28343	Lines are subset of the geometry base set. That is, lines are sets of points. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    ⇒   ⊢ (𝜑 → (𝑋𝐿𝑌) ⊆ 𝑃)
Theorem	tgellng 28344	Property of lying on the line going through points 𝑋 and 𝑌. Definition 4.10 of [Schwabhauser] p. 36. We choose the notation 𝑍 ∈ (𝑋(LineG‘𝐺)𝑌) instead of "colinear" because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
Theorem	tgcolg 28345	We choose the notation (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) instead of "colinear" in order to avoid defining an additional symbol for colinearity because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
Theorem	btwncolg1 28346	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌))    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
Theorem	btwncolg2 28347	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑍𝐼𝑌))    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
Theorem	btwncolg3 28348	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
Theorem	colcom 28349	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‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋))
Theorem	colrot1 28350	Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))
Theorem	colrot2 28351	Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑍𝐿𝑋) ∨ 𝑍 = 𝑋))
Theorem	ncolcom 28352	Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋))
Theorem	ncolrot1 28353	Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))
Theorem	ncolrot2 28354	Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → ¬ (𝑌 ∈ (𝑍𝐿𝑋) ∨ 𝑍 = 𝑋))
Theorem	tgdim01ln 28355	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 28356	If there are three non-colinear points, then the dimension is at least two. Converse of tglowdim2l 28441. (Contributed by Thierry Arnoux, 23-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))    ⇒   ⊢ (𝜑 → 𝐺DimTarskiG≥2)
Theorem	lnxfr 28357	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 28358*	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 28359	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 28360	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 28361	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 28362	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 28363	Lemma for tgbtwnconn1 28366. (Contributed by Thierry Arnoux, 30-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽))    &   ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷))    ⇒   ⊢ (𝜑 → 𝐻 = 𝐽)
Theorem	tgbtwnconn1lem2 28364	Lemma for tgbtwnconn1 28366. (Contributed by Thierry Arnoux, 30-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽))    &   ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐸 − 𝐹) = (𝐶 − 𝐷))
Theorem	tgbtwnconn1lem3 28365	Lemma for tgbtwnconn1 28366. (Contributed by Thierry Arnoux, 30-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽))    &   ⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐼𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐷𝐼𝐹))    &   ⊢ (𝜑 → 𝐶 ≠ 𝐸)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐹)
Theorem	tgbtwnconn1 28366	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 28367	Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
Theorem	tgbtwnconn3 28368	Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵)))
Theorem	tgbtwnconnln3 28369	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))    &   ⊢ 𝐿 = (LineG‘𝐺)    ⇒   ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
Theorem	tgbtwnconn22 28370	Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐸))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐷𝐼𝐸))
Theorem	tgbtwnconnln1 28371	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐷) ∨ 𝐶 = 𝐷))
Theorem	tgbtwnconnln2 28372	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 28373	Less-than relation for geometric congruences.
class ≤G
Definition	df-leg 28374*	Define the less-than relationship between geometric distance congruence classes. See legval 28375. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ ≤G = (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})
Theorem	legval 28375*	Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ≤ = {⟨𝑒, 𝑓⟩ ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))})
Theorem	legov 28376*	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 28377*	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 28378	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 28379	Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐴 − 𝐶))
Theorem	legtrd 28380	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 28381	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 28382	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 28383	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 28384	Deduce equality from "less than" null segments. (Contributed by Thierry Arnoux, 12-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	legbtwn 28385	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 28386	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 28387*	The set 𝐸 denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝐴 = (𝑥 − 𝑦))
Theorem	ltgov 28388	Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ ≤ = (≤G‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐸 = ( − “ (𝑃 × 𝑃))    &   ⊢ (𝜑 → Fun − )    &   ⊢ < = (( ≤ ↾ 𝐸) ∖ I )    &   ⊢ (𝜑 → (𝑃 × 𝑃) ⊆ dom − )    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) < (𝐶 − 𝐷) ↔ ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ∧ (𝐴 − 𝐵) ≠ (𝐶 − 𝐷))))
Theorem	legov3 28389	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 28390	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 28391	Function producing the relation "belong to the same half-line".
class hlG
Definition	df-hlg 28392*	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 28393	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 28394	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐵(𝐾‘𝐶)𝐴))
Theorem	hlcomd 28395	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵(𝐾‘𝐶)𝐴)
Theorem	hlne1 28396	The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	hlne2 28397	The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	hlln 28398	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 28399	The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝐵)
Theorem	hlid 28400	The half-line relation is reflexive. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐴)