P. 295 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29401-29500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	angmgmlem 29401*	Lemma for angmgm 29403. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ 𝐽 = (AngMgm‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))    ⇒   ⊢ (𝜑 → (𝐽 ∈ Mgm ∧ [⟨“𝑋𝑌𝑋”⟩] ∼ = (0g‘𝐽)))
Theorem	angmgm0g 29402*	The identity element of the angle addition magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ 𝐽 = (AngMgm‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))    ⇒   ⊢ (𝜑 → [⟨“𝑋𝑌𝑋”⟩] ∼ = (0g‘𝐽))
Theorem	angmgm 29403*	The angle addition magma is a magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ 𝐽 = (AngMgm‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 2 ≤ (♯‘𝑃))    ⇒   ⊢ (𝜑 → 𝐽 ∈ Mgm)
Theorem	angmgmbas 29404*	The base set of the angle addition magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐽 = (AngMgm‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → (𝐴 / ∼ ) = (Base‘𝐽))
16.2.20  Congruence Theorems
Theorem	tgsas1 29405	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 29406	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 29407	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 29408	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 29409	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 29410	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 29411	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 29412	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 29413	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 29414	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 28980, already covers that part: see trgcgr 28985. 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 28985. (Contributed by Thierry Arnoux, 18-Jan-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))
Theorem	isoas 29415	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.21  Equilateral triangles
Syntax	ceqlg 29416	Declare the class of equilateral triangles.
class eqltrG
Definition	df-eqlg 29417*	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 29418	Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺) ↔ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐵𝐶𝐴”⟩))
Theorem	iseqlgd 29419	Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐴 − 𝐵))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺))
16.2.22  Parallel lines
Syntax	cprlng 29420	Extend class notation for the parallel lines relation.
class parlnG
Definition	df-prlng 29421*	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 29422*	Property of two lines 𝐴 and 𝐵 to be parallel. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ∥ 𝐵 ↔ ((𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿) ∧ (𝐴 = 𝐵 ∨ (∃ℎ ∈ ran 𝐸(𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ) ∧ (𝐴 ∩ 𝐵) = ∅)))))
Theorem	prlngd 29423	Deduce parallelism between two lines 𝐴 and 𝐵. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐻)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → 𝐴 ∥ 𝐵)
Theorem	prlngref 29424	Parallelism is reflexive. Theorem 12.4 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    ⇒   ⊢ (𝜑 → 𝐴 ∥ 𝐴)
Theorem	prlngsym 29425	Parallelism is symmetric. Theorem 12.5 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 18-Jun-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∥ 𝐴)
Theorem	prlngrcl1 29426	Reverse closure for parallelism. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
Theorem	prlngrcl2 29427	Reverse closure for parallelism. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)
Theorem	prlngin0 29428	Two parallel lines do not intersect. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
Theorem	prlngpln 29429*	Two parallel lines are on a common plane. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∃ℎ ∈ ran 𝐸(𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ))
Theorem	prlnghpg 29430	If two lines 𝐴 and 𝐵 are parallel, then any two points 𝑋 and 𝑌 of 𝐵 lie on the same half-plane limited by 𝐴. Theorem 12.6 of [Schwabhauser] p. 122. . (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋((hpG‘𝐺)‘𝐴)𝑌)
Theorem	dfprlng2 29431	Alternate definition of (strict) parallelism. Theorem 12.7 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ (𝑃 ∖ {𝑍}))    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ≠ (𝑍𝐿𝑊))    ⇒   ⊢ (𝜑 → ((𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊) ↔ (𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∧ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑊)) = ∅)))
Theorem	dfprlng3 29432	Alternate definition of (strict) parallelism. Theorem 12.7 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐴 ≠ (𝑋𝐿𝑌))    ⇒   ⊢ (𝜑 → (𝐴 ∥ (𝑋𝐿𝑌) ↔ (𝑋((hpG‘𝐺)‘𝐴)𝑌 ∧ (𝐴 ∩ (𝑋𝐿𝑌)) = ∅)))
Theorem	prlngpln3 29433	Two parallel lines are on a common plane. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ (𝐴𝐸𝑋))
Theorem	perpprlng 29434	If two lines 𝐴 and 𝐵 have a common perpendicular 𝐶 and lie in the same plane 𝐻, then they are parallel. Theorem 12.9 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐶)    &   ⊢ (𝜑 → 𝐵(⟂G‘𝐺)𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∥ 𝐵)
Theorem	prlngex 29435*	There exists at least one parallel line 𝑏 to a given line 𝐴 through a given point 𝑋. Theorem 12.10 of [Schwabhauser] p. 122. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))
Theorem	prlngmolem1 29436*	Lemma for prlngmo 29438: Contradiction: Assuming two different parallels 𝐵 and 𝐶 having a common point 𝑋 exist to a line 𝐴, the geometry cannot be Euclidean (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ 𝐴))    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐵) ∧ 𝑏 ∈ (𝑃 ∖ 𝐵)) ∧ ∃𝑦 ∈ 𝐵 𝑦 ∈ (𝑎𝐼𝑏))}    &   ⊢ 𝑄 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐴) ∧ 𝑏 ∈ (𝑃 ∖ 𝐴)) ∧ ∃𝑤 ∈ 𝐴 𝑤 ∈ (𝑎𝐼𝑏))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐵 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐶 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ (𝐶 ∖ 𝐵))    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝑊𝑂𝑇)    ⇒   ⊢ (𝜑 → ¬ 𝐺 ∈ TarskiGE)
Theorem	prlngmolem2 29437*	Lemma for prlngmo 29438. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝑏) ∧ 𝑦 ∈ (𝑃 ∖ 𝑏)) ∧ ∃𝑟 ∈ 𝑏 𝑟 ∈ (𝑥(Itv‘𝐺)𝑦))}    &   ⊢ 𝑄 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝐴) ∧ 𝑦 ∈ (𝑃 ∖ 𝐴)) ∧ ∃𝑠 ∈ 𝐴 𝑠 ∈ (𝑥(Itv‘𝐺)𝑦))}    ⇒   ⊢ (𝜑 → ∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))
Theorem	prlngmo 29438*	Playfair's axiom. Given a line 𝐴 and a point 𝑋 not on 𝐴, at most one line parallel to 𝐴 can be drawn through 𝑋. Theorem 12.11 of [Schwabhauser] p. 123. Note that this is the first instance of a theorem where the geometry is required to be Euclidean, as expressed by 𝐺 ∈ TarskiGE. Theorem A10 of [Schwabhauser] p. 24 is used, in the form of axtgeucl 28940, in the proof of prlngmolem1 29436. See prlngex 29435 for the corresponding existence theorem. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    ⇒   ⊢ (𝜑 → ∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))
Theorem	prlngeu 29439*	Given a line 𝐴 and a point 𝑋 not on 𝐴, a unique line parallel to 𝐴 can be drawn through 𝑋. Theorem 12.13 of [Schwabhauser] p. 124. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    ⇒   ⊢ (𝜑 → ∃!𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))
Theorem	prlngmo2 29440*	Playfair's axiom, without the restriction that the point 𝑋 is outside of the line 𝐴. Theorem 12.11 of [Schwabhauser] p. 123. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    ⇒   ⊢ (𝜑 → ∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))
Theorem	prlngeq 29441	Playfair's axiom, written as an equality: if two different lines are parallel to a given line at a given point, they are equal. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	prlngpln4 29442	Building a parallel line conserves planes, i.e. given a line 𝐴 and a point 𝑋 not on 𝐴, the (unique) parallel 𝐵 to 𝐴 through 𝑋 lies completely within the plane defined by 𝐴 and 𝑋. Theorem 12.14 of [Schwabhauser] p. 124. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
Theorem	prlngplngtr 29443	Transitivity of parallelism, for lines in the same plane 𝐻. This is case 1 of Theorem 12.15 of [Schwabhauser] p. 124. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐵 ∥ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∥ 𝐶)
Theorem	prlnginn0 29444	A line 𝐶 intersecting another line 𝐴 also intersects any line 𝐵 parallel to 𝐴. Theorem 12.16 of [Schwabhauser] p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ ran 𝐿)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐶) ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐻)    ⇒   ⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅)
Theorem	prlngmid2 29445	If the midpoints of two segments (𝑋𝐼𝑍) and (𝑌𝐼𝑊) coincide, the points 𝑋, 𝑌, 𝑍 and 𝑊 form a parallelogram, i.e. the lines (𝑋𝐿𝑌) and (𝑍𝐿𝑊) are parallel. Theorem 12.17 of [Schwabhauser] p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ 𝑀 = (midG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋𝑀𝑍) = (𝑌𝑀𝑊))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    ⇒   ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))
Theorem	symquadprlng 29446	Symmetrical quadrilaterals are parallelograms. Theorem 12.18 of [Schwabhauser] p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑊))    &   ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑊 − 𝑋))    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    &   ⊢ (𝜑 → 𝑌 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑋𝐿𝑍))    &   ⊢ (𝜑 → 𝑇 ∈ (𝑌𝐿𝑊))    ⇒   ⊢ (𝜑 → ((𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊) ∧ (𝑌𝐿𝑍) ∥ (𝑊𝐿𝑋)))
Theorem	prlngsymquadlem 29447	Lemma for prlngsymquad 29448. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))    &   ⊢ (𝜑 → (𝑌𝐿𝑍) ∥ (𝑊𝐿𝑋))    &   ⊢ 𝑇 = (((pInvG‘𝐺)‘(𝑋(midG‘𝐺)𝑍))‘𝑌)    ⇒   ⊢ (𝜑 → 𝑇 = 𝑊)
Theorem	prlngsymquad 29448	All parallelograms are symmetric quadrilaterals. First part of Theorem 12.19 of [Schwabhauser] p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))    &   ⊢ (𝜑 → (𝑌𝐿𝑍) ∥ (𝑊𝐿𝑋))    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) = (𝑍 − 𝑊) ∧ (𝑌 − 𝑍) = (𝑊 − 𝑋)))
Theorem	prlngsymquadopp 29449*	In parallelograms, opposing vertices are on opposite sides of the diagonal. Second part of Theorem 12.19 of [Schwabhauser] p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))    &   ⊢ (𝜑 → (𝑌𝐿𝑍) ∥ (𝑊𝐿𝑋))    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑋𝐿𝑍)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑋𝐿𝑍))) ∧ ∃𝑡 ∈ (𝑋𝐿𝑍)𝑡 ∈ (𝑎𝐼𝑏))}    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝜑 → 𝑊𝑂𝑌)
Theorem	quadcgrprlng 29450*	Nontrivial quadrilaterals with congruent and parallel opposite sides are parallelograms. Theorem 12.20 of [Schwabhauser] p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑋𝐿𝑍)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑋𝐿𝑍))) ∧ ∃𝑡 ∈ (𝑋𝐿𝑍)𝑡 ∈ (𝑎𝐼𝑏))}    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → ¬ (𝑋 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))    &   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑊))    &   ⊢ (𝜑 → 𝑌𝑂𝑊)    ⇒   ⊢ (𝜑 → ((𝑌𝐿𝑍) ∥ (𝑊𝐿𝑋) ∧ (𝑌 − 𝑍) = (𝑊 − 𝑋)))
Theorem	tgaltai 29451*	Parallelism implies alternate angles congruence: if a line (𝑋𝐿𝑍) crosses two parallel lines (𝑋𝐿𝑌) and (𝑍𝐿𝑊), then the alternate angles are congruent. First direction of Theorem 12.21 of [Schwabhauser] p. 126. This is also Proposition 1.29 of Euclid's Elements . (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∥ = (parlnG‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑋𝐿𝑍)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑋𝐿𝑍))) ∧ ∃𝑡 ∈ (𝑋𝐿𝑍)𝑡 ∈ (𝑎𝐼𝑏))}    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))    &   ⊢ (𝜑 → 𝑌𝑂𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑍)    ⇒   ⊢ (𝜑 → ⟨“𝑌𝑋𝑍”⟩(cgrA‘𝐺)⟨“𝑊𝑍𝑋”⟩)
16.3  Properties of geometries
16.3.1  Isomorphisms between geometries
Theorem	f1otrgds 29452*	Convenient lemma for f1otrg 29454. (Contributed by Thierry Arnoux, 19-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐸𝑌) = ((𝐹‘𝑋)𝐷(𝐹‘𝑌)))
Theorem	f1otrgitv 29453*	Convenient lemma for f1otrg 29454. (Contributed by Thierry Arnoux, 19-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ 𝐽 = (Itv‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))    &   ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))))
Theorem	f1otrg 29454*	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 29455*	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 29456	Function to convert an algebraic structure to a Tarski geometry.
class toTG
Definition	df-ttg 29457*	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 29458*	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 29459	Lemma for ttgbas 29460, ttgvsca 29463 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 29460	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 29461	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 29462	The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ − = (-g‘𝐻)    ⇒   ⊢ − = (-g‘𝐺)
Theorem	ttgvsca 29463	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 29464	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 29465*	Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    ⇒   ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋𝐼𝑌) = {𝑧 ∈ 𝑃 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑋) = (𝑘 · (𝑌 − 𝑋))})
Theorem	ttgelitv 29466*	Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
⊢ 𝐺 = (toTG‘𝐻)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝑃 = (Base‘𝐻)    &   ⊢ − = (-g‘𝐻)    &   ⊢ · = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ ∃𝑘 ∈ (0[,]1)(𝑍 − 𝑋) = (𝑘 · (𝑌 − 𝑋))))
Theorem	ttgbtwnid 29467	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 29468	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 29469	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 29470*	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 29471	Declare the syntax for the Euclidean space generator.
class 𝔼
Syntax	cbtwn 29472	Declare the syntax for the Euclidean betweenness predicate.
class Btwn
Syntax	ccgr 29473	Declare the syntax for the Euclidean congruence predicate.
class Cgr
Definition	df-ee 29474	Define the Euclidean space generator. For details, see elee 29477. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑m (1...𝑛)))
Definition	df-btwn 29475*	Define the Euclidean betweenness predicate. For details, see brbtwn 29483. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ Btwn = ◡{⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}
Definition	df-cgr 29476*	Define the Euclidean congruence predicate. For details, see brcgr 29484. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ Cgr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑦 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) ∧ Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑥)‘𝑖) − ((2nd ‘𝑥)‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑛)((((1st ‘𝑦)‘𝑖) − ((2nd ‘𝑦)‘𝑖))↑2))}
Theorem	elee 29477	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 29478*	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 29479*	Obsolete version of mptelee 29478 as of 2-Feb-2026. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ))
Theorem	eleenn 29480	If 𝐴 is in (𝔼‘𝑁), then 𝑁 is a natural. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
Theorem	eleei 29481	The forward direction of elee 29477. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝐴:(1...𝑁)⟶ℝ)
Theorem	eedimeq 29482	A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑀)) → 𝑁 = 𝑀)
Theorem	brbtwn 29483*	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 29484*	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 29485	The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℝ)
Theorem	fveecn 29486	The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℂ)
Theorem	eqeefv 29487*	Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖)))
Theorem	eqeelen 29488*	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 29489*	Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))))
Theorem	colinearalglem1 29490	Lemma for colinearalg 29494. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (((𝐵 − 𝐴) · (𝐹 − 𝐷)) = ((𝐸 − 𝐷) · (𝐶 − 𝐴)) ↔ ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷)))))
Theorem	colinearalglem2 29491*	Lemma for colinearalg 29494. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))
Theorem	colinearalglem3 29492*	Lemma for colinearalg 29494. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑗) − (𝐶‘𝑗))) = (((𝐴‘𝑗) − (𝐶‘𝑗)) · ((𝐵‘𝑖) − (𝐶‘𝑖)))))
Theorem	colinearalglem4 29493*	Lemma for colinearalg 29494. 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 29494*	An algebraic characterization of colinearity. Note the similarity to brbtwn2 29489. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
Theorem	eleesub 29495*	Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖)))    ⇒   ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
Theorem	eleesubd 29496*	Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 29495. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ (𝜑 → 𝐶 = (𝑖 ∈ (1...𝑁) ↦ ((𝐴‘𝑖) − (𝐵‘𝑖))))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
16.4.2.2  Tarski's axioms for geometry for the Euclidean space
Theorem	axdimuniq 29497	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 29498	𝐴 is as far from 𝐵 as 𝐵 is from 𝐴. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐵, 𝐴⟩)
Theorem	axcgrtr 29499	Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩))
Theorem	axcgrid 29500	If there is no distance between 𝐴 and 𝐵, then 𝐴 = 𝐵. Axiom A3 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐶⟩ → 𝐴 = 𝐵))