P. 292 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	cgrg3col4 29101*	Lemma 11.28 of [Schwabhauser] p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
16.2.19  Congruence Theorems
Theorem	tgsas1 29102	First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then third sides are equal in length. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))
Theorem	tgsas 29103	First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then the triangles are congruent. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
Theorem	tgsas2 29104	First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩)
Theorem	tgsas3 29105	First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩)
Theorem	tgasa1 29106	Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩)    ⇒   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))
Theorem	tgasa 29107	Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
Theorem	tgsss1 29108	Third congruence theorem: SSS (Side-Side-Side): If the three pairs of sides of two triangles are equal in length, then the triangles are congruent. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
Theorem	tgsss2 29109	Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩)
Theorem	tgsss3 29110	Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩)
Theorem	dfcgrg2 29111	Congruence for two triangles can also be defined as congruence of sides and angles (6 parts). This is often the actual textbook definition of triangle congruence, see for example https://en.wikipedia.org/wiki/Congruence_(geometry)#Congruence_of_triangles. With this definition, the "SSS" congruence theorem has an additional part, namely, that triangle congruence implies congruence of the sides (which means equality of the lengths). Because our development of elementary geometry strives to closely follow Schwabhaeuser's, our original definition of shape congruence, df-cgrg 28734, already covers that part: see trgcgr 28739. This theorem is also named "CPCTC", which stands for "Corresponding Parts of Congruent Triangles are Congruent", see https://en.wikipedia.org/wiki/Congruence_(geometry)#CPCTC 28739. (Contributed by Thierry Arnoux, 18-Jan-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))
Theorem	isoas 29112	Congruence theorem for isocele triangles: if two angles of a triangle are congruent, then the corresponding sides also are. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐴𝐶𝐵”⟩)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐴 − 𝐶))
16.2.20  Equilateral triangles
Syntax	ceqlg 29113	Declare the class of equilateral triangles.
class eqltrG
Definition	df-eqlg 29114*	Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019.)
⊢ eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
Theorem	iseqlg 29115	Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺) ↔ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐵𝐶𝐴”⟩))
Theorem	iseqlgd 29116	Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐴 − 𝐵))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺))
16.2.21  Parallel lines
Syntax	cprlng 29117	Extend class notation for the parallel lines relation.
class parlnG
Definition	df-prlng 29118*	Define the parallel relation for lines. Definition 12.2 of [Schwabhauser] p. 121. Note that the textbook first defines a "strict" parallelism where equal lines are not considered parallel in the strict sense: here we jump directly to the more common definition which allows equality. (Contributed by Thierry Arnoux, 17-Jun-2026.)
⊢ parlnG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))})
Theorem	brprlng 29119*	Property of two lines 𝐴 and 𝐵 to be parallel. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ∥ 𝐵 ↔ ((𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿) ∧ (𝐴 = 𝐵 ∨ (∃ℎ ∈ ran 𝐸(𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ) ∧ (𝐴 ∩ 𝐵) = ∅)))))
Theorem	prlngd 29120	Deduce parallelism between two lines 𝐴 and 𝐵. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐻)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → 𝐴 ∥ 𝐵)
Theorem	prlngref 29121	Parallelism is reflexive. Theorem 12.4 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    ⇒   ⊢ (𝜑 → 𝐴 ∥ 𝐴)
Theorem	prlngsym 29122	Parallelism is symmetric. Theorem 12.5 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∥ 𝐴)
16.3  Properties of geometries
16.3.1  Isomorphisms between geometries
Theorem	f1otrgds 29123*	Convenient lemma for f1otrg 29125. (Contributed by Thierry Arnoux, 19-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = ((𝐹‘𝑋)𝐷(𝐹‘𝑌)))
Theorem	f1otrgitv 29124*	Convenient lemma for f1otrg 29125. (Contributed by Thierry Arnoux, 19-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))))
Theorem	f1otrg 29125*	A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))    ⇒   ⊢ (𝜑 → 𝐻 ∈ TarskiG)
Theorem	f1otrge 29126*	A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    ⇒   ⊢ (𝜑 → 𝐻 ∈ TarskiGE)
16.4  Geometry in Hilbert spaces
Syntax	cttg 29127	Function to convert an algebraic structure to a Tarski geometry.
class toTG
Definition	df-ttg 29128*	Define a function converting a subcomplex Hilbert space to a Tarski Geometry. It does so by equipping the structure with a betweenness operation. Note that because the scalar product is applied over the interval (0[,]1), only spaces whose scalar field is a superset of that interval can be considered. (Contributed by Thierry Arnoux, 24-Mar-2019.)
⊢ toTG = (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
Theorem	ttgval 29129*	Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof shortened by AV, 9-Nov-2024.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐻 ∈ 𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})))
Theorem	ttglem 29130	Lemma for ttgbas 29131, ttgvsca 29134 etc. (Contributed by Thierry Arnoux, 15-Apr-2019.) (Revised by AV, 29-Oct-2024.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (LineG‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Itv‘ndx)    ⇒   ⊢ (𝐸‘𝐻) = (𝐸‘𝐺)
Theorem	ttgbas 29131	The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ 𝐵 = (Base‘𝐺)
Theorem	ttgplusg 29132	The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ + = (+g‘𝐻)    ⇒   ⊢ + = (+g‘𝐺)
Theorem	ttgsub 29133	The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ − = (-g‘𝐻)    ⇒   ⊢ − = (-g‘𝐺)
Theorem	ttgvsca 29134	The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    ⇒   ⊢ · = ( ·𝑠 ‘𝐺)
Theorem	ttgds 29135	The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐷 = (dist‘𝐻)    ⇒   ⊢ 𝐷 = (dist‘𝐺)
Theorem	ttgitvval 29136*	Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    ⇒   ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋𝐼𝑌) = {𝑧 ∈ 𝑃 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑋) = (𝑘 · (𝑌 − 𝑋))})
Theorem	ttgelitv 29137*	Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝑍 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
Theorem	ttgbtwnid 29138	Any subcomplex module equipped with the betweenness operation fulfills the identity of betweenness (Axiom A6). (Contributed by Thierry Arnoux, 26-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ 𝑅 = (Base‘(Scalar‘𝐻))    &   ⊢ (𝜑 → (0[,]1) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝐻 ∈ ℂMod)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑋))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	ttgcontlem1 29139	Lemma for % ttgcont . (Contributed by Thierry Arnoux, 24-May-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ 𝑅 = (Base‘(Scalar‘𝐻))    &   ⊢ (𝜑 → (0[,]1) ⊆ 𝑅)    &   ⊢ + = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐻 ∈ ℂVec)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐾 ≠ 0)    &   ⊢ (𝜑 → 𝐾 ≠ 1)    &   ⊢ (𝜑 → 𝐿 ≠ 𝑀)    &   ⊢ (𝜑 → 𝐿 ≤ (𝑀 / 𝐾))    &   ⊢ (𝜑 → 𝐿 ∈ (0[,]1))    &   ⊢ (𝜑 → 𝐾 ∈ (0[,]1))    &   ⊢ (𝜑 → 𝑀 ∈ (0[,]𝐿))    &   ⊢ (𝜑 → (𝑋 − 𝐴) = (𝐾 · (𝑌 − 𝐴)))    &   ⊢ (𝜑 → (𝑋 − 𝐴) = (𝑀 · (𝑁 − 𝐴)))    &   ⊢ (𝜑 → 𝐵 = (𝐴 + (𝐿 · (𝑁 − 𝐴))))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝑋𝐼𝑌))
Theorem	xmstrkgc 29140	Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.)
⊢ (𝐺 ∈ ∞MetSp → 𝐺 ∈ TarskiGC)
16.4.1  Geometry in the complex plane
Theorem	cchhllem 29141*	Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019.) (Revised by AV, 29-Oct-2024.)
⊢ 𝐶 = (((subringAlg ‘ℂfld)‘ℝ) sSet ⟨(·𝑖‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · (∗‘𝑦)))⟩)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (Scalar‘ndx) ≠ (𝐸‘ndx)    &   ⊢ ( ·𝑠 ‘ndx) ≠ (𝐸‘ndx)    &   ⊢ (·𝑖‘ndx) ≠ (𝐸‘ndx)    ⇒   ⊢ (𝐸‘ℂfld) = (𝐸‘𝐶)
16.4.2  Geometry in Euclidean spaces
16.4.2.1  Definition of the Euclidean space
Syntax	cee 29142	Declare the syntax for the Euclidean space generator.
class 𝔼
Syntax	cbtwn 29143	Declare the syntax for the Euclidean betweenness predicate.
class Btwn
Syntax	ccgr 29144	Declare the syntax for the Euclidean congruence predicate.
class Cgr
Definition	df-ee 29145	Define the Euclidean space generator. For details, see elee 29148. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑m (1...𝑛)))
Definition	df-btwn 29146*	Define the Euclidean betweenness predicate. For details, see brbtwn 29154. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ Btwn = ◡{⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}
Definition	df-cgr 29147*	Define the Euclidean congruence predicate. For details, see brcgr 29155. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ Cgr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))}
Theorem	elee 29148	Membership in a Euclidean space. We define Euclidean space here using Cartesian coordinates over 𝑁 space. We later abstract away from this using Tarski's geometry axioms, so this exact definition is unimportant. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ (𝑁 ∈ ℕ → (𝐴 ∈ (𝔼‘𝑁) ↔ 𝐴:(1...𝑁)⟶ℝ))
Theorem	mptelee 29149*	A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by SN, 2-Feb-2026.)
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ))
Theorem	mpteleeOLD 29150*	Obsolete version of mptelee 29149 as of 2-Feb-2026. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ))
Theorem	eleenn 29151	If 𝐴 is in (𝔼‘𝑁), then 𝑁 is a natural. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
Theorem	eleei 29152	The forward direction of elee 29148. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝐴:(1...𝑁)⟶ℝ)
Theorem	eedimeq 29153	A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑀)) → 𝑁 = 𝑀)
Theorem	brbtwn 29154*	The binary relation form of the betweenness predicate. The statement 𝐴 Btwn ⟨𝐵, 𝐶⟩ should be informally read as "𝐴 lies on a line segment between 𝐵 and 𝐶. This exact definition is abstracted away by Tarski's geometry axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
Theorem	brcgr 29155*	The binary relation form of the congruence predicate. The statement ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ should be read informally as "the 𝑁 dimensional point 𝐴 is as far from 𝐵 as 𝐶 is from 𝐷, or "the line segment 𝐴𝐵 is congruent to the line segment 𝐶𝐷. This particular definition is encapsulated by Tarski's axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)))
Theorem	fveere 29156	The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℝ)
Theorem	fveecn 29157	The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℂ)
Theorem	eqeefv 29158*	Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖)))
Theorem	eqeelen 29159*	Two points are equal iff the square of the distance between them is zero. (Contributed by Scott Fenton, 10-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = 0))
Theorem	brbtwn2 29160*	Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))))
Theorem	colinearalglem1 29161	Lemma for colinearalg 29165. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (((𝐵 − 𝐴) · (𝐹 − 𝐷)) = ((𝐸 − 𝐷) · (𝐶 − 𝐴)) ↔ ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷)))))
Theorem	colinearalglem2 29162*	Lemma for colinearalg 29165. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))
Theorem	colinearalglem3 29163*	Lemma for colinearalg 29165. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑗) − (𝐶‘𝑗))) = (((𝐴‘𝑗) − (𝐶‘𝑗)) · ((𝐵‘𝑖) − (𝐶‘𝑖)))))
Theorem	colinearalglem4 29164*	Lemma for colinearalg 29165. Prove a disjunction that will be needed in the final proof. (Contributed by Scott Fenton, 27-Jun-2013.)
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0))
Theorem	colinearalg 29165*	An algebraic characterization of colinearity. Note the similarity to brbtwn2 29160. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
Theorem	eleesub 29166*	Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖)))    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
Theorem	eleesubd 29167*	Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 29166. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ (𝜑 → 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖))))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
16.4.2.2  Tarski's axioms for geometry for the Euclidean space
Theorem	axdimuniq 29168	The unique dimension axiom. If a point is in 𝑁 dimensional space and in 𝑀 dimensional space, then 𝑁 = 𝑀. This axiom is not traditionally presented with Tarski's axioms, but we require it here as we are considering spaces in arbitrary dimensions. (Contributed by Scott Fenton, 24-Sep-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑀 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑀))) → 𝑁 = 𝑀)
Theorem	axcgrrflx 29169	𝐴 is as far from 𝐵 as 𝐵 is from 𝐴. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐵, 𝐴⟩)
Theorem	axcgrtr 29170	Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩))
Theorem	axcgrid 29171	If there is no distance between 𝐴 and 𝐵, then 𝐴 = 𝐵. Axiom A3 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐶⟩ → 𝐴 = 𝐵))
Theorem	axsegconlem1 29172*	Lemma for axsegcon 29182. Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013.)
⊢ ((𝐴 = 𝐵 ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝑥‘𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝑥‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)))
Theorem	axsegconlem2 29173*	Lemma for axsegcon 29182. Show that the square of the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝑆 ∈ ℝ)
Theorem	axsegconlem3 29174*	Lemma for axsegcon 29182. Show that the square of the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 0 ≤ 𝑆)
Theorem	axsegconlem4 29175*	Lemma for axsegcon 29182. Show that the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (√‘𝑆) ∈ ℝ)
Theorem	axsegconlem5 29176*	Lemma for axsegcon 29182. Show that the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 0 ≤ (√‘𝑆))
Theorem	axsegconlem6 29177*	Lemma for axsegcon 29182. Show that the distance between two distinct points is positive. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 0 < (√‘𝑆))
Theorem	axsegconlem7 29178*	Lemma for axsegcon 29182. Show that a particular ratio of distances is in the closed unit interval. (Contributed by Scott Fenton, 18-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    &   ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)    ⇒   ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((√‘𝑆) / ((√‘𝑆) + (√‘𝑇))) ∈ (0[,]1))
Theorem	axsegconlem8 29179*	Lemma for axsegcon 29182. Show that a particular mapping generates a point. (Contributed by Scott Fenton, 18-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    &   ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)    &   ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))    ⇒   ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
Theorem	axsegconlem9 29180*	Lemma for axsegcon 29182. Show that 𝐵𝐹 is congruent to 𝐶𝐷. (Contributed by Scott Fenton, 19-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    &   ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)    &   ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))    ⇒   ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
Theorem	axsegconlem10 29181*	Lemma for axsegcon 29182. Show that the scaling constant from axsegconlem7 29178 produces the betweenness condition for 𝐴, 𝐵 and 𝐹. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    &   ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)    &   ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))    ⇒   ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − ((√‘𝑆) / ((√‘𝑆) + (√‘𝑇)))) · (𝐴‘𝑖)) + (((√‘𝑆) / ((√‘𝑆) + (√‘𝑇))) · (𝐹‘𝑖))))
Theorem	axsegcon 29182*	Any segment 𝐴𝐵 can be extended to a point 𝑥 such that 𝐵𝑥 is congruent to 𝐶𝐷. Axiom A4 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 4-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐵, 𝑥⟩Cgr⟨𝐶, 𝐷⟩))
Theorem	ax5seglem1 29183*	Lemma for ax5seg 29193. Rexpress a one congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐵‘𝑗))↑2) = ((𝑇↑2) · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)))
Theorem	ax5seglem2 29184*	Lemma for ax5seg 29193. Rexpress another congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐶‘𝑗))↑2) = (((1 − 𝑇)↑2) · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)))
Theorem	ax5seglem3a 29185	Lemma for ax5seg 29193. (Contributed by Scott Fenton, 7-May-2015.)
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑗 ∈ (1...𝑁)) → (((𝐴‘𝑗) − (𝐶‘𝑗)) ∈ ℝ ∧ ((𝐷‘𝑗) − (𝐹‘𝑗)) ∈ ℝ))
Theorem	ax5seglem3 29186*	Lemma for ax5seg 29193. Combine congruences for points on a line. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑆) · (𝐷‘𝑖)) + (𝑆 · (𝐹‘𝑖))))) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)) → Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2) = Σ𝑗 ∈ (1...𝑁)(((𝐷‘𝑗) − (𝐹‘𝑗))↑2))
Theorem	ax5seglem4 29187*	Lemma for ax5seg 29193. Given two distinct points, the scaling constant in a betweenness statement is nonzero. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐵) → 𝑇 ≠ 0)
Theorem	ax5seglem5 29188*	Lemma for ax5seg 29193. If 𝐵 is between 𝐴 and 𝐶, and 𝐴 is distinct from 𝐵, then 𝐴 is distinct from 𝐶. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝐵 ∧ 𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2) ≠ 0)
Theorem	ax5seglem6 29189*	Lemma for ax5seg 29193. Given two line segments that are divided into pieces, if the pieces are congruent, then the scaling constant is the same. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)))) ∧ (𝐴 ≠ 𝐵 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑆) · (𝐷‘𝑖)) + (𝑆 · (𝐹‘𝑖))))) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)) → 𝑇 = 𝑆)
Theorem	ax5seglem7 29190	Lemma for ax5seg 29193. An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑇 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))))
Theorem	ax5seglem8 29191	Lemma for ax5seg 29193. Use the weak deduction theorem to eliminate the hypotheses from ax5seglem7 29190. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝑇 · ((𝐶 − 𝐷)↑2)) = ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))))
Theorem	ax5seglem9 29192*	Lemma for ax5seg 29193. Take the calculation in ax5seglem8 29191 and turn it into a series of measurements. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.)
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = (Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))))
Theorem	ax5seg 29193	The five segment axiom. Take two triangles 𝐴𝐷𝐶 and 𝐸𝐻𝐺, a point 𝐵 on 𝐴𝐶, and a point 𝐹 on 𝐸𝐺. If all corresponding line segments except for 𝐶𝐷 and 𝐺𝐻 are congruent, then so are 𝐶𝐷 and 𝐺𝐻. Axiom A5 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
Theorem	axbtwnid 29194	Points are indivisible. That is, if 𝐴 lies between 𝐵 and 𝐵, then 𝐴 = 𝐵. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐵⟩ → 𝐴 = 𝐵))
Theorem	axpaschlem 29195*	Lemma for axpasch 29196. Set up coefficients used in the proof. (Contributed by Scott Fenton, 5-Jun-2013.)
⊢ ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
Theorem	axpasch 29196*	The inner Pasch axiom. Take a triangle 𝐴𝐶𝐸, a point 𝐷 on 𝐴𝐶, and a point 𝐵 extending 𝐶𝐸. Then 𝐴𝐸 and 𝐷𝐵 intersect at some point 𝑥. Axiom A7 of [Schwabhauser] p. 12. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩)))
Theorem	axlowdimlem1 29197	Lemma for axlowdim 29216. Establish a particular constant function as a function. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ ((3...𝑁) × {0}):(3...𝑁)⟶ℝ
Theorem	axlowdimlem2 29198	Lemma for axlowdim 29216. Show that two sets are disjoint. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ ((1...2) ∩ (3...𝑁)) = ∅
Theorem	axlowdimlem3 29199	Lemma for axlowdim 29216. Set up a union property for an interval of integers. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (1...𝑁) = ((1...2) ∪ (3...𝑁)))
Theorem	axlowdimlem4 29200	Lemma for axlowdim 29216. Set up a particular constant function. (Contributed by Scott Fenton, 17-Apr-2013.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ {⟨1, 𝐴⟩, ⟨2, 𝐵⟩}:(1...2)⟶ℝ