P. 289 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28801-28900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isinag 28801*	Property for point 𝑋 to lie in the angle ⟨“𝐴𝐵𝐶”⟩. Definition 11.23 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩ ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋)))))
Theorem	isinagd 28802	Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → (𝑌 = 𝐵 ∨ 𝑌(𝐾‘𝐵)𝑋))    ⇒   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
Theorem	inagflat 28803	Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
Theorem	inagswap 28804	Swap the order of the half lines delimiting the angle. Theorem 11.24 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐶𝐵𝐴”⟩)
Theorem	inagne1 28805	Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	inagne2 28806	Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐵)
Theorem	inagne3 28807	Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝐵)
Theorem	inaghl 28808	The "point lie in angle" relation is independent of the points chosen on the half lines starting from 𝐵. Theorem 11.25 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 27-Sep-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷(𝐾‘𝐵)𝐴)    &   ⊢ (𝜑 → 𝐹(𝐾‘𝐵)𝐶)    &   ⊢ (𝜑 → 𝑌(𝐾‘𝐵)𝑋)    ⇒   ⊢ (𝜑 → 𝑌(inA‘𝐺)⟨“𝐷𝐵𝐹”⟩)
Definition	df-leag 28809*	Definition of the geometrical "angle less than" relation. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.)
⊢ ≤∠ = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
Theorem	isleag 28810*	Geometrical "less than" property for angles. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ∃𝑥 ∈ 𝑃 (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)))
Theorem	isleagd 28811	Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ ≤ = (≤∠‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑋”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ≤ ⟨“𝐷𝐸𝐹”⟩)
Theorem	leagne1 28812	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	leagne2 28813	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐵)
Theorem	leagne3 28814	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐷 ≠ 𝐸)
Theorem	leagne4 28815	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐹 ≠ 𝐸)
Theorem	cgrg3col4 28816*	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.18  Congruence Theorems
Theorem	tgsas1 28817	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 28818	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 28819	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 28820	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 28821	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 28822	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 28823	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 28824	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 28825	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 28826	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 28474, already covers that part: see trgcgr 28479. 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 28479. (Contributed by Thierry Arnoux, 18-Jan-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))
Theorem	isoas 28827	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.19  Equilateral triangles
Syntax	ceqlg 28828	Declare the class of equilateral triangles.
class eqltrG
Definition	df-eqlg 28829*	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 28830	Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺) ↔ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐵𝐶𝐴”⟩))
Theorem	iseqlgd 28831	Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐴 − 𝐵))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺))
16.3  Properties of geometries
16.3.1  Isomorphisms between geometries
Theorem	f1otrgds 28832*	Convenient lemma for f1otrg 28834. (Contributed by Thierry Arnoux, 19-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = ((𝐹‘𝑋)𝐷(𝐹‘𝑌)))
Theorem	f1otrgitv 28833*	Convenient lemma for f1otrg 28834. (Contributed by Thierry Arnoux, 19-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))))
Theorem	f1otrg 28834*	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 28835*	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 28836	Function to convert an algebraic structure to a Tarski geometry.
class toTG
Definition	df-ttg 28837*	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 28838*	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 28839	Lemma for ttgbas 28840, ttgvsca 28843 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 28840	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 28841	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 28842	The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ − = (-g‘𝐻)    ⇒   ⊢ − = (-g‘𝐺)
Theorem	ttgvsca 28843	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 28844	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 28845*	Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    ⇒   ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋𝐼𝑌) = {𝑧 ∈ 𝑃 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑋) = (𝑘 · (𝑌 − 𝑋))})
Theorem	ttgelitv 28846*	Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝑍 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
Theorem	ttgbtwnid 28847	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 28848	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 28849	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 28850*	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 28851	Declare the syntax for the Euclidean space generator.
class 𝔼
Syntax	cbtwn 28852	Declare the syntax for the Euclidean betweenness predicate.
class Btwn
Syntax	ccgr 28853	Declare the syntax for the Euclidean congruence predicate.
class Cgr
Definition	df-ee 28854	Define the Euclidean space generator. For details, see elee 28857. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑m (1...𝑛)))
Definition	df-btwn 28855*	Define the Euclidean betweenness predicate. For details, see brbtwn 28862. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ Btwn = ◡{⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}
Definition	df-cgr 28856*	Define the Euclidean congruence predicate. For details, see brcgr 28863. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ Cgr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))}
Theorem	elee 28857	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 28858*	A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.)
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ))
Theorem	eleenn 28859	If 𝐴 is in (𝔼‘𝑁), then 𝑁 is a natural. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
Theorem	eleei 28860	The forward direction of elee 28857. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝐴:(1...𝑁)⟶ℝ)
Theorem	eedimeq 28861	A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑀)) → 𝑁 = 𝑀)
Theorem	brbtwn 28862*	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 28863*	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 28864	The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℝ)
Theorem	fveecn 28865	The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℂ)
Theorem	eqeefv 28866*	Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖)))
Theorem	eqeelen 28867*	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 28868*	Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))))
Theorem	colinearalglem1 28869	Lemma for colinearalg 28873. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (((𝐵 − 𝐴) · (𝐹 − 𝐷)) = ((𝐸 − 𝐷) · (𝐶 − 𝐴)) ↔ ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷)))))
Theorem	colinearalglem2 28870*	Lemma for colinearalg 28873. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))
Theorem	colinearalglem3 28871*	Lemma for colinearalg 28873. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑗) − (𝐶‘𝑗))) = (((𝐴‘𝑗) − (𝐶‘𝑗)) · ((𝐵‘𝑖) − (𝐶‘𝑖)))))
Theorem	colinearalglem4 28872*	Lemma for colinearalg 28873. 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 28873*	An algebraic characterization of colinearity. Note the similarity to brbtwn2 28868. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
Theorem	eleesub 28874*	Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖)))    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
Theorem	eleesubd 28875*	Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 28874. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ (𝜑 → 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖))))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
16.4.2.2  Tarski's axioms for geometry for the Euclidean space
Theorem	axdimuniq 28876	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 28877	𝐴 is as far from 𝐵 as 𝐵 is from 𝐴. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐵, 𝐴⟩)
Theorem	axcgrtr 28878	Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩))
Theorem	axcgrid 28879	If there is no distance between 𝐴 and 𝐵, then 𝐴 = 𝐵. Axiom A3 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐶⟩ → 𝐴 = 𝐵))
Theorem	axsegconlem1 28880*	Lemma for axsegcon 28890. Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013.)
⊢ ((𝐴 = 𝐵 ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝑥‘𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝑥‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)))
Theorem	axsegconlem2 28881*	Lemma for axsegcon 28890. 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 28882*	Lemma for axsegcon 28890. Show that the square of the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 0 ≤ 𝑆)
Theorem	axsegconlem4 28883*	Lemma for axsegcon 28890. Show that the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (√‘𝑆) ∈ ℝ)
Theorem	axsegconlem5 28884*	Lemma for axsegcon 28890. Show that the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 0 ≤ (√‘𝑆))
Theorem	axsegconlem6 28885*	Lemma for axsegcon 28890. Show that the distance between two distinct points is positive. (Contributed by Scott Fenton, 17-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 0 < (√‘𝑆))
Theorem	axsegconlem7 28886*	Lemma for axsegcon 28890. 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 28887*	Lemma for axsegcon 28890. Show that a particular mapping generates a point. (Contributed by Scott Fenton, 18-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    &   ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)    &   ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))    ⇒   ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁))
Theorem	axsegconlem9 28888*	Lemma for axsegcon 28890. Show that 𝐵𝐹 is congruent to 𝐶𝐷. (Contributed by Scott Fenton, 19-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    &   ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)    &   ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))    ⇒   ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
Theorem	axsegconlem10 28889*	Lemma for axsegcon 28890. Show that the scaling constant from axsegconlem7 28886 produces the betweenness condition for 𝐴, 𝐵 and 𝐹. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)    &   ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)    &   ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))    ⇒   ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − ((√‘𝑆) / ((√‘𝑆) + (√‘𝑇)))) · (𝐴‘𝑖)) + (((√‘𝑆) / ((√‘𝑆) + (√‘𝑇))) · (𝐹‘𝑖))))
Theorem	axsegcon 28890*	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 28891*	Lemma for ax5seg 28901. 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 28892*	Lemma for ax5seg 28901. 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 28893	Lemma for ax5seg 28901. (Contributed by Scott Fenton, 7-May-2015.)
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑗 ∈ (1...𝑁)) → (((𝐴‘𝑗) − (𝐶‘𝑗)) ∈ ℝ ∧ ((𝐷‘𝑗) − (𝐹‘𝑗)) ∈ ℝ))
Theorem	ax5seglem3 28894*	Lemma for ax5seg 28901. 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 28895*	Lemma for ax5seg 28901. 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 28896*	Lemma for ax5seg 28901. 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 28897*	Lemma for ax5seg 28901. 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 28898	Lemma for ax5seg 28901. An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑇 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))))
Theorem	ax5seglem8 28899	Lemma for ax5seg 28901. Use the weak deduction theorem to eliminate the hypotheses from ax5seglem7 28898. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝑇 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝑇 · ((𝐶 − 𝐷)↑2)) = ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))))
Theorem	ax5seglem9 28900*	Lemma for ax5seg 28901. Take the calculation in ax5seglem8 28899 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)))))