P. 293 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29201-29300   *Has distinct variable group(s)

Type	Label	Description
Statement
16.2.17  Congruence of angles
Syntax	ccgra 29201	Declare the constant for the congruence between angles relation.
class cgrA
Definition	df-cgra 29202*	Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 29203 for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020.)
⊢ cgrA = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
Theorem	iscgra 29203*	Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of [Schwabhauser] p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 29225 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑥𝐸𝑦”⟩ ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹)))
Theorem	iscgra1 29204*	A special version of iscgra 29203 where one distance is known to be equal. In this case, angle congruence can be written with only one quantifier. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ∃𝑥 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑥”⟩ ∧ 𝑥(𝐾‘𝐸)𝐹)))
Theorem	iscgrad 29205	Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑋𝐸𝑌”⟩)    &   ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐷)    &   ⊢ (𝜑 → 𝑌(𝐾‘𝐸)𝐹)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
Theorem	cgrane1 29206	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	cgrane2 29207	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	cgrane3 29208	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐸 ≠ 𝐷)
Theorem	cgrane4 29209	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐸 ≠ 𝐹)
Theorem	cgrahl1 29210	Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐷)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝑋𝐸𝐹”⟩)
Theorem	cgrahl2 29211	Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝐹)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑋”⟩)
Theorem	cgracgr 29212	First direction of proposition 11.4 of [Schwabhauser] p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋(𝐾‘𝐵)𝐴)    &   ⊢ (𝜑 → 𝑌(𝐾‘𝐵)𝐶)    &   ⊢ (𝜑 → (𝐵 − 𝑋) = (𝐸 − 𝐷))    &   ⊢ (𝜑 → (𝐵 − 𝑌) = (𝐸 − 𝐹))    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐷 − 𝐹))
Theorem	cgraid 29213	Angle congruence is reflexive. Theorem 11.6 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 31-Jul-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
Theorem	cgraswap 29214	Swap rays in a congruence relation. Theorem 11.9 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐶𝐵𝐴”⟩)
Theorem	cgrcgra 29215	Triangle congruence implies angle congruence. This is a portion of CPCTC, focusing on a specific angle. (Contributed by Arnoux, 2-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
Theorem	cgracom 29216	Angle congruence commutes. Theorem 11.7 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
Theorem	cgratr 29217	Angle congruence is transitive. Theorem 11.8 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐻𝑈𝐽”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐻𝑈𝐽”⟩)
Theorem	zerocgra 29218	Zero angles are congruent. Zero angles, that is, angles of degree zero, can be expressed by stating that points 𝐴 and 𝐶 are on the same ray starting at 𝐵, that is, 𝐴(𝐾‘𝐵)𝐶. See also flatcgra 29219. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐵)𝐶)    &   ⊢ (𝜑 → 𝐷(𝐾‘𝐸)𝐹)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
Theorem	flatcgra 29219	Flat angles are congruent. Flat angles, or straight angles, represent half a turn. They can be represented by points ⟨“𝐴𝐵𝐶”⟩ where 𝐵 is on the segment (𝐴𝐼𝐶). (Contributed by Thierry Arnoux, 13-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐸)    &   ⊢ (𝜑 → 𝐹 ≠ 𝐸)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
Theorem	cgraswaplr 29220	Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐶𝐵𝐴”⟩(cgrA‘𝐺)⟨“𝐹𝐸𝐷”⟩)
Theorem	cgrabtwn 29221	Angle congruence preserves flat angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))
Theorem	cgrahl 29222	Angle congruence preserves null angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐴(𝐾‘𝐵)𝐶)    ⇒   ⊢ (𝜑 → 𝐷(𝐾‘𝐸)𝐹)
Theorem	cgracol 29223	Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
Theorem	cgrancol 29224	Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
Theorem	dfcgra2 29225*	This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 29202 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))))
Theorem	sacgr 29226	Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020.) (Proof shortened by Igor Ieskov, 16-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝑌))    &   ⊢ (𝜑 → 𝐵 ≠ 𝑋)    &   ⊢ (𝜑 → 𝐸 ≠ 𝑌)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝑌𝐸𝐹”⟩)
Theorem	oacgr 29227	Vertical angle theorem. Vertical, or opposite angles are the facing pair of angles formed when two lines intersect. Eudemus of Rhodes attributed the proof to Thales of Miletus. The proposition showed that since both of a pair of vertical angles are supplementary to both of the adjacent angles, the vertical angles are equal in measure. We follow the same path. Theorem 11.14 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 27-Sep-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐹))    &   ⊢ (𝜑 → 𝐵 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐷)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐹)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐵𝐹”⟩)
Theorem	acopy 29228*	Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))    &   ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
Theorem	acopyeu 29229	Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points 𝑋 and 𝑌 both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))    &   ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑋”⟩)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑌”⟩)    &   ⊢ (𝜑 → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)    &   ⊢ (𝜑 → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)    ⇒   ⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝑌)
Theorem	ragcgra 29230	Right angles are congruent with each other. Theorem 11.16 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∈ (∟G‘𝐺))    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
Theorem	cgrarag 29231	Any angle ⟨“𝐴𝐵𝐶”⟩ congruent with a right angle ⟨“𝑋𝑌𝑍”⟩ is a right angle. Theorem 11.17 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∈ (∟G‘𝐺))    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (∟G‘𝐺))
Theorem	ragsupplcgra 29232	An angle ⟨“𝑋𝑌𝑍”⟩ is a right angle exactly when it is congruent to its supplementary angle ⟨“𝑋𝑌𝑊”⟩. Theorem 11.18 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 13-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ {𝑌}))    &   ⊢ (𝜑 → 𝑊 ∈ (𝑃 ∖ {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐼𝑊))    ⇒   ⊢ (𝜑 → (⟨“𝑋𝑌𝑍”⟩ ∈ (∟G‘𝐺) ↔ ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑊”⟩))
Theorem	ragraghl 29233	Drawing two right angles at a point 𝑋 on the same side of a line (𝑋𝐿𝑌) leads to points 𝑊 and 𝑍 on the same ray from 𝑋. Theorem 11.19 of [Schwabhauser] p. 99. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → ⟨“𝑌𝑋𝑍”⟩ ∈ (∟G‘𝐺))    &   ⊢ (𝜑 → ⟨“𝑌𝑋𝑊”⟩ ∈ (∟G‘𝐺))    &   ⊢ (𝜑 → 𝑍((hpG‘𝐺)‘(𝑌𝐿𝑋))𝑊)    ⇒   ⊢ (𝜑 → 𝑍((hlG‘𝐺)‘𝑋)𝑊)
Theorem	perpeqlem 29234	Lemma for perpeq 29235. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐻)    &   ⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)    &   ⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴)    &   ⊢ (𝜑 → 𝑌((hpG‘𝐺)‘𝐴)𝑍)    ⇒   ⊢ (𝜑 → (𝑋𝐿𝑌) = (𝑋𝐿𝑍))
Theorem	perpeq 29235	Uniqueness of the perpendicular to a line 𝐴 within a plane 𝐻 at a point 𝑋. Theorem 11.20 of [Schwabhauser] p. 99. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ 𝐸 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)    &   ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐻)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐻)    &   ⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)    &   ⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴)    ⇒   ⊢ (𝜑 → (𝑋𝐿𝑌) = (𝑋𝐿𝑍))
Theorem	tgaaddcpbllem1 29236*	Lemma for tgaaddcpbl 29239. (Contributed by Thierry Arnoux, 2-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}    &   ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑆)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑇)    &   ⊢ (𝜑 → 𝑋𝑂𝑍)    &   ⊢ (𝜑 → 𝑈𝑄𝑊)    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)    &   ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑋𝐼𝑍))    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ (𝑌𝐿𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐼𝑍))    &   ⊢ (𝜑 → 𝑅(𝐾‘𝑌)𝑆)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
Theorem	tgaaddcpbllem2 29237*	Lemma for tgaaddcpbl 29239. (Contributed by Thierry Arnoux, 2-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}    &   ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑆)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑇)    &   ⊢ (𝜑 → 𝑋𝑂𝑍)    &   ⊢ (𝜑 → 𝑈𝑄𝑊)    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)    &   ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑋𝐼𝑍))    &   ⊢ (𝜑 → 𝑅 ∈ (𝑌𝐿𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐼𝑍))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑆𝐼𝑅))    &   ⊢ 𝑀 = ((pInvG‘𝐺)‘𝑉)    &   ⊢ 𝐾 = (hlG‘𝐺)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
Theorem	tgaaddcpbllem3 29238*	Lemma for tgaaddcpbl 29239. (Contributed by Thierry Arnoux, 2-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}    &   ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑆)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑇)    &   ⊢ (𝜑 → 𝑋𝑂𝑍)    &   ⊢ (𝜑 → 𝑈𝑄𝑊)    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)    &   ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)    &   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑋𝐼𝑍))    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
Theorem	tgaaddcpbl 29239*	The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Theorem 11.22 of [Schwabhauser] p. 99. The angles ⟨“𝑋𝑌𝑆”⟩ and ⟨“𝑆𝑌𝑍”⟩ are added to result in ⟨“𝑋𝑌𝑍”⟩, and ⟨“𝑈𝑉𝑇”⟩ and ⟨“𝑇𝑉𝑊”⟩ are added to result in ⟨“𝑈𝑉𝑊”⟩. (Contributed by Thierry Arnoux, 2-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}    &   ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑆)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑇)    &   ⊢ (𝜑 → 𝑋𝑂𝑍)    &   ⊢ (𝜑 → 𝑈𝑄𝑊)    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)    &   ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
Theorem	tgaaddcpbl2 29240	The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Compared with tgaaddcpbl 29239, this version handles cases where 𝑈, 𝑉 and 𝑊 are aligned. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑆)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑇)    &   ⊢ (𝜑 → ((𝑌𝐿𝑆) ∩ (𝑋𝐼𝑍)) ≠ ∅)    &   ⊢ (𝜑 → ((𝑉𝐿𝑇) ∩ (𝑈𝐼𝑊)) ≠ ∅)    &   ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)    &   ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
16.2.18  Angle Comparisons
Syntax	cinag 29241	Extend class relation with the geometrical "point in angle" relation.
class inA
Syntax	cleag 29242	Extend class relation with the "angle less than" relation.
class ≤∠
Definition	df-inag 29243*	Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020.)
⊢ inA = (𝑔 ∈ V ↦ {⟨𝑝, 𝑡⟩ ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))})
Theorem	isinag 29244*	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 29245	Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → (𝑌 = 𝐵 ∨ 𝑌(𝐾‘𝐵)𝑋))    ⇒   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
Theorem	inagflat 29246	Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
Theorem	inagswap 29247	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 29248	Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	inagne2 29249	Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐵)
Theorem	inagne3 29250	Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐾 = (hlG‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐴𝐵𝐶”⟩)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝐵)
Theorem	inaghl 29251	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 29252*	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 29253*	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 29254	Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ ≤ = (≤∠‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑋”⟩)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ≤ ⟨“𝐷𝐸𝐹”⟩)
Theorem	leagne1 29255	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	leagne2 29256	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐵)
Theorem	leagne3 29257	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐷 ≠ 𝐸)
Theorem	leagne4 29258	Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)    ⇒   ⊢ (𝜑 → 𝐹 ≠ 𝐸)
Theorem	cgrg3col4 29259*	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  Angle Addition
Syntax	cangmgm 29260	Extend class relation with the "angle addition" magma.
class AngMgm
Definition	df-angmgm 29261*	Definition of the angle addition magma. See following theorems for better readable properties. Because the textbook's definition of angle congruence does not consider orientation (cf. cgraswap 29214) , our notion of angle does not include reflex angles (angles larger than a straight angle). Therefore, like with ℕ0, at this point, we can only build a magma , which is e.g. not isomorphic with the rotation group SO(2) . (Contributed by Thierry Arnoux, 20-Jul-2026.)
⊢ AngMgm = (𝑔 ∈ V ↦ ⦋(Base‘𝑔) / 𝑝⦌⦋{𝑑 ∈ (𝑝 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} / 𝑎⦌({⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩} /s (cgrA‘𝑔)))
Theorem	elcgrabasi 29262*	Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 ∈ V    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ (𝜑 → 𝐸 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝐸 = ⟨“𝑥𝑦𝑧”⟩ ∧ (𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧)))
Theorem	elcgrabasrd 29263*	Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ (𝜑 → 𝑃 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∈ 𝐴)
Theorem	cgraer 29264*	The angle congruence relation is an equivalence relation. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ( ∼ ∩ (𝐴 × 𝐴)) Er 𝐴)
Theorem	cgrabasimass 29265*	The angle congruence relation is hereditary. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → ( ∼ “ 𝐴) ⊆ 𝐴)
Theorem	angmgmaddeu1 29266*	There exists a unique point 𝑠 satisfying the conditions of angle addition. General case. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍))    &   ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑉𝐿𝑊))    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))
Theorem	angmgmaddeu2 29267*	Existence of a unique point for building angle addition. Case where the second angle is a zero angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍))    &   ⊢ (𝜑 → 𝑈((hlG‘𝐺)‘𝑉)𝑊)    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))
Theorem	angmgmaddeu3 29268*	Existence of a unique point for building angle addition. Case where the second angle is a flat angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍))    &   ⊢ (𝜑 → 𝑉 ∈ (𝑈𝐼𝑊))    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))
Theorem	angmgmaddeu4 29269*	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where both angles are zero angles. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → 𝑋((hlG‘𝐺)‘𝑌)𝑍)    &   ⊢ (𝜑 → 𝑈((hlG‘𝐺)‘𝑉)𝑊)    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))
Theorem	angmgmaddeu5 29270*	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where one angle is a zero angle, and the other angle is a straight angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → 𝑋((hlG‘𝐺)‘𝑌)𝑍)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑈𝐼𝑊))    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))
Theorem	angmgmaddeu6 29271*	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where the first angle is a zero angle, and the second angle is a straight angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))    &   ⊢ (𝜑 → 𝑈((hlG‘𝐺)‘𝑉)𝑊)    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))
Theorem	angmgmaddeu7 29272*	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where both angles are straight angles. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))    &   ⊢ (𝜑 → 𝑉 ∈ (𝑈𝐼𝑊))    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))
Theorem	angmgmaddov1lem 29273*	Lemma for angmgmaddov1 29275. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍))    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))
Theorem	angmgmaddov2lem 29274*	Lemma for angmgmaddov2 29276. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍))    ⇒   ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑊𝑉𝑠”⟩ ∼ ⟨“𝑋𝑌𝑍”⟩ ∧ (𝑉 − 𝑠) = (𝑌 − 𝑋)))
Theorem	angmgmaddov1 29275*	Value of the addition operation in the angle addition magma, in case the first angle is neither zero nor flat. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝑍𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)    &   ⊢ (𝜑 → (𝑌 − 𝑆) = (𝑉 − 𝑈))    &   ⊢ (𝜑 → ((𝑌𝐿𝑍) ∩ (𝑆𝐼𝑋)) ≠ ∅)    ⇒   ⊢ (𝜑 → (⟨“𝑋𝑌𝑍”⟩ + ⟨“𝑈𝑉𝑊”⟩) = ⟨“𝑋𝑌𝑆”⟩)
Theorem	angmgmaddov2 29276*	Value of the addition operation in the angle addition magma, in case the first angle is zero or flat. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑉 ≠ 𝑊)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑍)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝑊𝑉𝑆”⟩ ∼ ⟨“𝑋𝑌𝑍”⟩)    &   ⊢ (𝜑 → (𝑉 − 𝑆) = (𝑌 − 𝑋))    ⇒   ⊢ (𝜑 → (⟨“𝑋𝑌𝑍”⟩ + ⟨“𝑈𝑉𝑊”⟩) = ⟨“𝑈𝑉𝑆”⟩)
Theorem	angmgmaddcpbl 29277*	Addition of angles is compatible with angle congruence. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∼ 𝐶)    &   ⊢ (𝜑 → 𝐹 ∼ 𝐷)    ⇒   ⊢ (𝜑 → (𝐸 + 𝐹) ∼ (𝐶 + 𝐷))
Theorem	angmgmaddcl 29278*	Closure of the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐸 + 𝐹) ∈ 𝐴)
Theorem	angmgmaddlid 29279*	The left identity element for the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (⟨“𝑋𝑌𝑋”⟩ + 𝐸) ∼ 𝐸)
Theorem	angmgmaddrid 29280*	The right identity element for the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
Theorem	angmgmval 29281*	Explicit the value of the angle addition magma for a given geometry 𝐺. (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‘𝐺)    &   ⊢ ≤ = (≤∠‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐽 = ({⟨(Base‘ndx), 𝐴⟩, ⟨(+g‘ndx), + ⟩, ⟨(le‘ndx), ≤ ⟩} /s ∼ ))
Theorem	angmgmlem 29282*	Lemma for angmgm 29284. (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 29283*	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 29284*	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 29285*	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 29286	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 29287	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 29288	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 29289	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 29290	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 29291	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 29292	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 29293	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 29294	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 29295	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 28861, already covers that part: see trgcgr 28866. 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 28866. (Contributed by Thierry Arnoux, 18-Jan-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))
Theorem	isoas 29296	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 29297	Declare the class of equilateral triangles.
class eqltrG
Definition	df-eqlg 29298*	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 29299	Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺) ↔ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐵𝐶𝐴”⟩))
Theorem	iseqlgd 29300	Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐴 − 𝐵))    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ (eqltrG‘𝐺))