P. 285 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28401-28500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zs12negsclb 28401	A surreal is a dyadic fraction iff its negative is. (Contributed by Scott Fenton, 9-Nov-2025.)
⊢ (𝐴 ∈ No → (𝐴 ∈ ℤs[1/2] ↔ ( -us ‘𝐴) ∈ ℤs[1/2]))
Theorem	zs12zodd 28402*	A dyadic fraction is either an integer or an odd number divided by a positive power of two. (Contributed by Scott Fenton, 5-Dec-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → (𝐴 ∈ ℤs ∨ ∃𝑥 ∈ ℤs ∃𝑦 ∈ ℕs 𝐴 = (((2s ·s 𝑥) +s 1s ) /su (2s↑s𝑦))))
Theorem	zs12ge0 28403*	An expression for non-negative dyadic rationals. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴) → (𝐴 ∈ ℤs[1/2] ↔ ∃𝑥 ∈ ℕ0s ∃𝑦 ∈ ℕ0s ∃𝑝 ∈ ℕ0s (𝐴 = (𝑥 +s (𝑦 /su (2s↑s𝑝))) ∧ 𝑦 <s (2s↑s𝑝))))
Theorem	zs12bday 28404	A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝐴 ∈ ℤs[1/2] → ( bday ‘𝐴) ∈ ω)
15.6.6  Real numbers
Syntax	creno 28405	Declare the syntax for the surreal reals.
class ℝs
Definition	df-reno 28406*	Define the surreal reals. These are the finite numbers without any infintesimal parts. Definition from [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ℝs = {𝑥 ∈ No ∣ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}
Theorem	elreno 28407*	Membership in the set of surreal reals. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s /su 𝑛))}))))
Theorem	recut 28408*	The cut involved in defining surreal reals is a genuine cut. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s /su 𝑛))})
Theorem	0reno 28409	Surreal zero is a surreal real. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 0s ∈ ℝs
Theorem	renegscl 28410	The surreal reals are closed under negation. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℝs → ( -us ‘𝐴) ∈ ℝs)
Theorem	readdscl 28411	The surreal reals are closed under addition. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℝs ∧ 𝐵 ∈ ℝs) → (𝐴 +s 𝐵) ∈ ℝs)
Theorem	remulscllem1 28412*	Lemma for remulscl 28414. Split a product of reciprocals of naturals. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs 𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s ( 1s /su 𝑞))) ↔ ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛)))
Theorem	remulscllem2 28413*	Lemma for remulscl 28414. Bound 𝐴 and 𝐵 above and below. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ((𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs) ∧ ((( -us ‘𝑁) <s 𝐴 ∧ 𝐴 <s 𝑁) ∧ (( -us ‘𝑀) <s 𝐵 ∧ 𝐵 <s 𝑀)))) → ∃𝑝 ∈ ℕs (( -us ‘𝑝) <s (𝐴 ·s 𝐵) ∧ (𝐴 ·s 𝐵) <s 𝑝))
Theorem	remulscl 28414	The surreal reals are closed under multiplication. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ ℝs ∧ 𝐵 ∈ ℝs) → (𝐴 ·s 𝐵) ∈ ℝs)
PART 16  ELEMENTARY GEOMETRY This part develops elementary geometry based on Tarski's axioms, following [Schwabhauser]. Tarski's geometry is a first-order theory with one sort, the "points". It has two primitive notions, the ternary predicate of "betweenness" and the quaternary predicate of "congruence". To adapt this theory to the framework of set.mm, and to be able to talk of *a* Tarski structure as a space satisfying the given axioms, we use the following definition, stated informally: A Tarski structure 𝑓 is a set (of points) (Base‘𝑓) together with functions (Itv‘𝑓) and (dist‘𝑓) on ((Base‘𝑓) × (Base‘𝑓)) satisfying certain axioms (given in Definitions df-trkg 28441 et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct 17068). The translation to and from Tarski's treatment is as follows (given, again, informally). Suppose that one is given an extensible structure 𝑓. One defines a betweenness ternary predicate Btw by positing that, for any 𝑥, 𝑦, 𝑧 ∈ (Base‘𝑓), one has "Btw 𝑥𝑦𝑧 " if and only if 𝑦 ∈ 𝑥(Itv‘𝑓)𝑧, and a congruence quaternary predicate Congr by positing that, for any 𝑥, 𝑦, 𝑧, 𝑡 ∈ (Base‘𝑓), one has "Congr 𝑥𝑦𝑧𝑡 " if and only if 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡. It is easy to check that if 𝑓 satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when (Base‘𝑓) is interpreted as the universe of discourse. Conversely, suppose that one is given a set 𝑎, a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure 𝑓 such that (Base‘𝑓) is 𝑎, and (Itv‘𝑓) is the function which associates with each ⟨𝑥, 𝑦⟩ ∈ (𝑎 × 𝑎) the set of points 𝑧 ∈ 𝑎 such that "Btw 𝑥𝑧𝑦", and (dist‘𝑓) is the function which associates with each ⟨𝑥, 𝑦⟩ ∈ (𝑎 × 𝑎) the set of ordered pairs ⟨𝑧, 𝑡⟩ ∈ (𝑎 × 𝑎) such that "Congr 𝑥𝑦𝑧𝑡". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when 𝑎 is interpreted as the universe of discourse, then 𝑓 satisfies our Tarski axioms. We intentionally choose to represent congruence (without loss of generality) as 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡 instead of "Congr 𝑥𝑦𝑧𝑡", as it is more convenient. It is always possible to define dist for any particular geometry to produce equal results when congruence is desired, and in many cases there is an obvious interpretation of "distance" between two points that can be useful in other situations. Encoding congruence as an equality of distances makes it easier to use these theorems in cases where there is a preferred distance function. We prove that representing a congruence relationship using a distance in the form 𝑥(dist‘𝑓)𝑦 = 𝑧(dist‘𝑓)𝑡 causes no loss of generality in tgjustc1 28463 and tgjustc2 28464, which in turn are supported by tgjustf 28461 and tgjustr 28462. A similar representation of congruence (using a "distance" function) is used in Axiom A1 of [Beeson2016] p. 5, which discusses how a large number of formalized proofs were found in Tarskian Geometry using OTTER. Their detailed proofs in Tarski Geometry, along with other information, are available at https://www.michaelbeeson.com/research/FormalTarski/ 28462. Most theorems are in deduction form, as this is a very general, simple, and convenient format to use in Metamath. An assertion in deduction form can be easily converted into an assertion in inference form (removing the antecedents 𝜑 →) by insert a ⊤ → in each hypothesis, using a1i 11, then using mptru 1548 to remove the final ⊤ → prefix. In some cases we represent, without loss of generality, an implication antecedent in [Schwabhauser] as a hypothesis. The implication can be retrieved from the by using simpr 484, the theorem as stated, and ex 412. For descriptions of individual axioms, we refer to the specific definitions below. A particular feature of Tarski's axioms is modularity, so by using various subsets of the set of axioms, we can define the classes of "absolute dimensionless Tarski structures" (df-trkg 28441), of "Euclidean dimensionless Tarski structures" (df-trkge 28439) and of "Tarski structures of dimension no less than N" (df-trkgld 28440). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 28796 and iscgra 28797). To maintain its simplicity, in this system congruence between shapes (a finite sequence of points) is the case where corresponding segments between all corresponding points are congruent. This includes triangles (a shape of 3 distinct points). Note that this definition has no direct regard for angles. For more details and rationale, see df-cgrg 28499. The first section is devoted to the definitions of these various structures. The second section ("Tarskian geometry") develops the synthetic treatment of geometry. The remaining sections prove that real Euclidean spaces and complex Hilbert spaces, with intended interpretations, are Euclidean Tarski structures. Most of the work in this part is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. See also the credits in the comment of each statement.
16.1  Definition and Tarski's Axioms of Geometry
Syntax	cstrkg 28415	Extends class notation with the class of Tarski geometries.
class TarskiG
Syntax	cstrkgc 28416	Extends class notation with the class of geometries fulfilling the congruence axioms.
class TarskiGC
Syntax	cstrkgb 28417	Extends class notation with the class of geometries fulfilling the betweenness axioms.
class TarskiGB
Syntax	cstrkgcb 28418	Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms.
class TarskiGCB
Syntax	cstrkgld 28419	Extends class notation with the relation for geometries fulfilling the lower dimension axioms.
class DimTarskiG≥
Syntax	cstrkge 28420	Extends class notation with the class of geometries fulfilling Euclid's axiom.
class TarskiGE
Syntax	citv 28421	Declare the syntax for the Interval (segment) index extractor.
class Itv
Syntax	clng 28422	Declare the syntax for the Line function.
class LineG
Definition	df-itv 28423	Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) Use its index-independent form itvid 28427 instead. (New usage is discouraged.)
⊢ Itv = Slot ;16
Definition	df-lng 28424	Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.) Use its index-independent form lngid 28428 instead. (New usage is discouraged.)
⊢ LineG = Slot ;17
Theorem	itvndx 28425	Index value of the Interval (segment) slot. Use ndxarg 17117. (Contributed by Thierry Arnoux, 24-Aug-2017.) (New usage is discouraged.)
⊢ (Itv‘ndx) = ;16
Theorem	lngndx 28426	Index value of the "line" slot. Use ndxarg 17117. (Contributed by Thierry Arnoux, 27-Mar-2019.) (New usage is discouraged.)
⊢ (LineG‘ndx) = ;17
Theorem	itvid 28427	Utility theorem: index-independent form of df-itv 28423. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ Itv = Slot (Itv‘ndx)
Theorem	lngid 28428	Utility theorem: index-independent form of df-lng 28424. (Contributed by Thierry Arnoux, 27-Mar-2019.)
⊢ LineG = Slot (LineG‘ndx)
Theorem	slotsinbpsd 28429	The slots Base, +g, ·𝑠 and dist are different from the slot Itv. Formerly part of ttglem 28864 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ (((Itv‘ndx) ≠ (Base‘ndx) ∧ (Itv‘ndx) ≠ (+g‘ndx)) ∧ ((Itv‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (Itv‘ndx) ≠ (dist‘ndx)))
Theorem	slotslnbpsd 28430	The slots Base, +g, ·𝑠 and dist are different from the slot LineG. Formerly part of ttglem 28864 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ (((LineG‘ndx) ≠ (Base‘ndx) ∧ (LineG‘ndx) ≠ (+g‘ndx)) ∧ ((LineG‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (LineG‘ndx) ≠ (dist‘ndx)))
Theorem	lngndxnitvndx 28431	The slot for the line is not the slot for the Interval (segment) in an extensible structure. Formerly part of proof for ttgval 28863. (Contributed by AV, 9-Nov-2024.)
⊢ (LineG‘ndx) ≠ (Itv‘ndx)
Theorem	trkgstr 28432	Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝑈⟩, ⟨(dist‘ndx), 𝐷⟩, ⟨(Itv‘ndx), 𝐼⟩}    ⇒   ⊢ 𝑊 Struct ⟨1, ;16⟩
Theorem	trkgbas 28433	The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝑈⟩, ⟨(dist‘ndx), 𝐷⟩, ⟨(Itv‘ndx), 𝐼⟩}    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝑈 = (Base‘𝑊))
Theorem	trkgdist 28434	The measure of a distance in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝑈⟩, ⟨(dist‘ndx), 𝐷⟩, ⟨(Itv‘ndx), 𝐼⟩}    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐷 = (dist‘𝑊))
Theorem	trkgitv 28435	The congruence relation in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝑈⟩, ⟨(dist‘ndx), 𝐷⟩, ⟨(Itv‘ndx), 𝐼⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐼 = (Itv‘𝑊))
Definition	df-trkgc 28436*	Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2753, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ TarskiGC = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))}
Definition	df-trkgb 28437*	Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.)
⊢ TarskiGB = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))}
Definition	df-trkgcb 28438*	Define the class of geometries fulfilling the five segment axiom, Axiom A5 of [Schwabhauser] p. 11, and segment construction axiom, Axiom A4 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ TarskiGCB = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑝 ∀𝑐 ∈ 𝑝 ∀𝑣 ∈ 𝑝 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))}
Definition	df-trkge 28439*	Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ TarskiGE = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))}
Definition	df-trkgld 28440*	Define the class of geometries fulfilling the lower dimension axiom for dimension 𝑛. For such geometries, there are three non-colinear points that are equidistant from 𝑛 − 1 distinct points. Derived from remarks in Tarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.) (Revised by Thierry Arnoux, 23-Nov-2019.)
⊢ DimTarskiG≥ = {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
Definition	df-trkg 28441*	Define the class of Tarski geometries. A Tarski geometry is a set of points, equipped with a betweenness relation (denoting that a point lies on a line segment between two other points) and a congruence relation (denoting equality of line segment lengths). Here, we are using the following: for congruence, (𝑥 − 𝑦) = (𝑧 − 𝑤) where − = (dist‘𝑊) for betweenness, 𝑦 ∈ (𝑥𝐼𝑧), where 𝐼 = (Itv‘𝑊) With this definition, the axiom A2 is actually equivalent to the transitivity of equality, eqtrd 2768. Tarski originally had more axioms, but later reduced his list to 11: A1 A kind of reflexivity for the congruence relation (TarskiGC) A2 Transitivity for the congruence relation (TarskiGC) A3 Identity for the congruence relation (TarskiGC) A4 Axiom of segment construction (TarskiGCB) A5 5-segment axiom (TarskiGCB) A6 Identity for the betweenness relation (TarskiGB) A7 Axiom of Pasch (TarskiGB) A8 Lower dimension axiom (◡DimTarskiG≥ “ {2}) A9 Upper dimension axiom (V ∖ (◡DimTarskiG≥ “ {3})) A10 Euclid's axiom (TarskiGE) A11 Axiom of continuity (TarskiGB) Our definition is split into 5 parts: congruence axioms TarskiGC (which metric spaces fulfill) betweenness axioms TarskiGB congruence and betweenness axioms TarskiGCB upper and lower dimension axioms DimTarskiG≥ axiom of Euclid / parallel postulate TarskiGE So our definition of a Tarskian Geometry includes the 3 axioms for the quaternary congruence relation (A1, A2, A3), the 3 axioms for the ternary betweenness relation (A6, A7, A11), and the 2 axioms of compatibility of the congruence and the betweenness relations (A4,A5). It does not include Euclid's axiom A10, nor the 2-dimensional axioms A8 (Lower dimension axiom) and A9 (Upper dimension axiom) so the number of dimensions of the geometry it formalizes is not constrained. Considering A2 as one of the 3 axioms for the quaternary congruence relation is somewhat conventional, because the transitivity of the congruence relation is automatically given by our choice to take the distance as this congruence relation in our definition of Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) (Revised by Thierry Arnoux, 27-Apr-2019.)
⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
Theorem	istrkgc 28442*	Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦))))
Theorem	istrkgb 28443*	Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiGB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎 ∈ 𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃∀𝑡 ∈ 𝒫 𝑃(∃𝑎 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐼𝑦)))))
Theorem	istrkgcb 28444*	Property of being a Tarski geometry - congruence and betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))))
Theorem	istrkge 28445*	Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiGE ↔ (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
Theorem	istrkgl 28446*	Building lines from the segment property. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐺 ∈ V ∧ (LineG‘𝐺) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})))
Theorem	istrkgld 28447*	Property of fulfilling the lower dimension 𝑁 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝐺DimTarskiG≥𝑁 ↔ ∃𝑓(𝑓:(1..^𝑁)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^𝑁)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
Theorem	istrkg2ld 28448*	Property of fulfilling the lower dimension 2 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥2 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
Theorem	istrkg3ld 28449*	Property of fulfilling the lower dimension 3 axiom. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥3 ↔ ∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 (𝑢 ≠ 𝑣 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
Theorem	axtgcgrrflx 28450	Axiom of reflexivity of congruence, Axiom A1 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑌 − 𝑋))
Theorem	axtgcgrid 28451	Axiom of identity of congruence, Axiom A3 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	axtgsegcon 28452*	Axiom of segment construction, Axiom A4 of [Schwabhauser] p. 11. As discussed in Axiom 4 of [Tarski1999] p. 178, "The intuitive content [is that] given any line segment 𝐴𝐵, one can construct a line segment congruent to it, starting at any point 𝑌 and going in the direction of any ray containing 𝑌. The ray is determined by the point 𝑌 and a second point 𝑋, the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point 𝑧 whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵)))
Theorem	axtg5seg 28453	Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. Take two triangles 𝑋𝑍𝑈 and 𝐴𝐶𝑉, a point 𝑌 on 𝑋𝑍, and a point 𝐵 on 𝐴𝐶. If all corresponding line segments except for 𝑍𝑈 and 𝐶𝑉 are congruent ( i.e., 𝑋𝑌 ∼ 𝐴𝐵, 𝑌𝑍 ∼ 𝐵𝐶, 𝑋𝑈 ∼ 𝐴𝑉, and 𝑌𝑈 ∼ 𝐵𝑉), then 𝑍𝑈 and 𝐶𝑉 are also congruent. As noted in Axiom 5 of [Tarski1999] p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵))    &   ⊢ (𝜑 → (𝑌 − 𝑍) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝑋 − 𝑈) = (𝐴 − 𝑉))    &   ⊢ (𝜑 → (𝑌 − 𝑈) = (𝐵 − 𝑉))    ⇒   ⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉))
Theorem	axtgbtwnid 28454	Identity of Betweenness. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑋))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	axtgpasch 28455*	Axiom of (Inner) Pasch, Axiom A7 of [Schwabhauser] p. 12. Given triangle 𝑋𝑌𝑍, point 𝑈 in segment 𝑋𝑍, and point 𝑉 in segment 𝑌𝑍, there exists a point 𝑎 on both the segment 𝑈𝑌 and the segment 𝑉𝑋. This axiom is essentially a subset of the general Pasch axiom. The general Pasch axiom asserts that on a plane "a line intersecting a triangle in one of its sides, and not intersecting any of the vertices, must intersect one of the other two sides" (per the discussion about Axiom 7 of [Tarski1999] p. 179). The (general) Pasch axiom was used implicitly by Euclid, but never stated; Moritz Pasch discovered its omission in 1882. As noted in the Metamath book, this means that the omission of Pasch's axiom from Euclid went unnoticed for 2000 years. Only the inner Pasch algorithm is included as an axiom; the "outer" form of the Pasch axiom can be proved using the inner form (see theorem 9.6 of [Schwabhauser] p. 69 and the brief discussion in axiom 7.1 of [Tarski1999] p. 180). (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ (𝑋𝐼𝑍))    &   ⊢ (𝜑 → 𝑉 ∈ (𝑌𝐼𝑍))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 (𝑎 ∈ (𝑈𝐼𝑌) ∧ 𝑎 ∈ (𝑉𝐼𝑋)))
Theorem	axtgcont1 28456*	Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. This axiom (scheme) asserts that any two sets 𝑆 and 𝑇 (of points) such that the elements of 𝑆 precede the elements of 𝑇 with respect to some point 𝑎 (that is, 𝑥 is between 𝑎 and 𝑦 whenever 𝑥 is in 𝑋 and 𝑦 is in 𝑌) are separated by some point 𝑏; this is explained in Axiom 11 of [Tarski1999] p. 185. (Contributed by Thierry Arnoux, 16-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑃)    ⇒   ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
Theorem	axtgcont 28457*	Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. For more information see axtgcont1 28456. (Contributed by Thierry Arnoux, 16-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇) → 𝑢 ∈ (𝐴𝐼𝑣))    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ 𝑃 ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 𝑏 ∈ (𝑥𝐼𝑦))
Theorem	axtglowdim2 28458*	Lower dimension axiom for dimension 2, Axiom A8 of [Schwabhauser] p. 13. There exist 3 non-colinear points. (Contributed by Thierry Arnoux, 20-Nov-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺DimTarskiG≥2)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))
Theorem	axtgupdim2 28459	Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. Three points 𝑋, 𝑌 and 𝑍 equidistant to two given two points 𝑈 and 𝑉 must be colinear. (Contributed by Thierry Arnoux, 29-May-2019.) (Revised by Thierry Arnoux, 11-Jul-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → (𝑈 − 𝑋) = (𝑉 − 𝑋))    &   ⊢ (𝜑 → (𝑈 − 𝑌) = (𝑉 − 𝑌))    &   ⊢ (𝜑 → (𝑈 − 𝑍) = (𝑉 − 𝑍))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐺DimTarskiG≥3)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
Theorem	axtgeucl 28460*	Euclid's Axiom. Axiom A10 of [Schwabhauser] p. 13. This is equivalent to Euclid's parallel postulate when combined with other axioms. (Contributed by Thierry Arnoux, 16-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiGE)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ (𝑋𝐼𝑉))    &   ⊢ (𝜑 → 𝑈 ∈ (𝑌𝐼𝑍))    &   ⊢ (𝜑 → 𝑋 ≠ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))
16.1.1  Justification for the congruence notation
Theorem	tgjustf 28461*	Given any function 𝐹, equality of the image by 𝐹 is an equivalence relation. (Contributed by Thierry Arnoux, 25-Jan-2023.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑟(𝑟 Er 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑟𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦))))
Theorem	tgjustr 28462*	Given any equivalence relation 𝑅, one can define a function 𝑓 such that all elements of an equivalence classe of 𝑅 have the same image by 𝑓. (Contributed by Thierry Arnoux, 25-Jan-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦))))
Theorem	tgjustc1 28463*	A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    ⇒   ⊢ ∃𝑟(𝑟 Er (𝑃 × 𝑃) ∧ ∀𝑤 ∈ 𝑃 ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (⟨𝑤, 𝑥⟩𝑟⟨𝑦, 𝑧⟩ ↔ (𝑤 − 𝑥) = (𝑦 − 𝑧)))
Theorem	tgjustc2 28464*	A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝑅 Er (𝑃 × 𝑃)    ⇒   ⊢ ∃𝑑(𝑑 Fn (𝑃 × 𝑃) ∧ ∀𝑤 ∈ 𝑃 ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (⟨𝑤, 𝑥⟩𝑅⟨𝑦, 𝑧⟩ ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧)))
16.2  Tarskian Geometry
16.2.1  Congruence
Theorem	tgcgrcomimp 28465	Congruence commutes on the RHS. Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by David A. Wheeler, 29-Jun-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) = (𝐶 − 𝐷) → (𝐴 − 𝐵) = (𝐷 − 𝐶)))
Theorem	tgcgrcomr 28466	Congruence commutes on the RHS. Variant of Theorem 2.5 of [Schwabhauser] p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐶))
Theorem	tgcgrcoml 28467	Congruence commutes on the LHS. Variant of Theorem 2.5 of [Schwabhauser] p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐶 − 𝐷))
Theorem	tgcgrcomlr 28468	Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶))
Theorem	tgcgreqb 28469	Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
Theorem	tgcgreq 28470	Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	tgcgrneq 28471	Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	tgcgrtriv 28472	Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐴) = (𝐵 − 𝐵))
Theorem	tgcgrextend 28473	Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019.) (Shortened by David A. Wheeler and Thierry Arnoux, 22-Apr-2020.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹))
Theorem	tgsegconeq 28474	Two points that satisfy the conclusion of axtgsegcon 28452 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐷𝐼𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐷𝐼𝐹))    &   ⊢ (𝜑 → (𝐴 − 𝐸) = (𝐵 − 𝐶))    &   ⊢ (𝜑 → (𝐴 − 𝐹) = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐸 = 𝐹)
16.2.2  Betweenness
Theorem	tgbtwntriv2 28475	Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐵))
Theorem	tgbtwncom 28476	Betweenness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴))
Theorem	tgbtwncomb 28477	Betweenness commutes, biconditional version. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ↔ 𝐵 ∈ (𝐶𝐼𝐴)))
Theorem	tgbtwnne 28478	Betweenness and inequality. (Contributed by Thierry Arnoux, 1-Dec-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ≠ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	tgbtwntriv1 28479	Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐼𝐵))
Theorem	tgbtwnswapid 28480	If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 16-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	tgbtwnintr 28481	Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐷))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐷))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
Theorem	tgbtwnexch3 28482	Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷))
Theorem	tgbtwnouttr2 28483	Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷))    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))
Theorem	tgbtwnexch2 28484	Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷))    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))
Theorem	tgbtwnouttr 28485	Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))
Theorem	tgbtwnexch 28486	Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))
Theorem	tgtrisegint 28487*	A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of [Schwabhauser] p. 33. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐶))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐷))    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝑃 (𝑞 ∈ (𝐹𝐼𝐶) ∧ 𝑞 ∈ (𝐵𝐼𝐸)))
16.2.3  Dimension
Theorem	tglowdim1 28488*	Lower dimension axiom for one dimension. In dimension at least 1, there are at least two distinct points. The condition "the space is of dimension 1 or more" is written here as 2 ≤ (♯‘𝑃) to avoid a new definition, but a different convention could be chosen. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 2 ≤ (♯‘𝑃))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 𝑥 ≠ 𝑦)
Theorem	tglowdim1i 28489*	Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 2 ≤ (♯‘𝑃))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝑃 𝑋 ≠ 𝑦)
Theorem	tgldimor 28490	Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019.)
⊢ 𝑃 = (𝐸‘𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤ (♯‘𝑃)))
Theorem	tgldim0eq 28491	In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 11-Apr-2019.)
⊢ 𝑃 = (𝐸‘𝐹)    &   ⊢ (𝜑 → (♯‘𝑃) = 1)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	tgldim0itv 28492	In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 12-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (♯‘𝑃) = 1)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶))
Theorem	tgldim0cgr 28493	In dimension zero, any two pairs of points are congruent. (Contributed by Thierry Arnoux, 12-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → (♯‘𝑃) = 1)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))
Theorem	tgbtwndiff 28494*	There is always a 𝑐 distinct from 𝐵 such that 𝐵 lies between 𝐴 and 𝑐. Theorem 3.14 of [Schwabhauser] p. 32. The condition "the space is of dimension 1 or more" is written here as 2 ≤ (♯‘𝑃) for simplicity. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 2 ≤ (♯‘𝑃))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 (𝐵 ∈ (𝐴𝐼𝑐) ∧ 𝐵 ≠ 𝑐))
Theorem	tgdim01 28495	In geometries of dimension less than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐺DimTarskiG≥2)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
16.2.4  Betweenness and Congruence
Theorem	tgifscgr 28496	Inner five segment congruence. Take two triangles, 𝐴𝐷𝐶 and 𝐸𝐻𝐾, with 𝐵 between 𝐴 and 𝐶 and 𝐹 between 𝐸 and 𝐾. If the other components of the triangles are congruent, then so are 𝐵𝐷 and 𝐹𝐻. Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐸𝐼𝐾))    &   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐸 − 𝐾))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐹 − 𝐾))    &   ⊢ (𝜑 → (𝐴 − 𝐷) = (𝐸 − 𝐻))    &   ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐾 − 𝐻))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐷) = (𝐹 − 𝐻))
Theorem	tgcgrsub 28497	Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))    &   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹))    &   ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))
16.2.5  Congruence of a series of points
Syntax	ccgrg 28498	Declare the constant for the congruence between shapes relation.
class cgrG
Definition	df-cgrg 28499*	Define the relation of congruence between shapes. Definition 4.4 of [Schwabhauser] p. 35. A "shape" is a finite sequence of points, and a triangle can be represented as a shape with three points. Two shapes are congruent if all corresponding segments between all corresponding points are congruent. Many systems of geometry define triangle congruence as requiring both segment congruence and angle congruence. Such systems, such as Hilbert's axiomatic system, typically have a primitive notion of angle congruence in addition to segment congruence. Here, angle congruence is instead a derived notion, defined later in df-cgra 28796 and expanded in iscgra 28797. This does not mean our system is weaker; dfcgrg2 28851 proves that these two definitions are equivalent, and using the Tarski definition instead (given in [Schwabhauser] p. 35) is simpler. Once two triangles are proven congruent as defined here, you can use various theorems to prove that corresponding parts of congruent triangles are congruent (CPCTC). For example, see cgr3simp1 28508, cgr3simp2 28509, cgr3simp3 28510, cgrcgra 28809, and permutation laws such as cgr3swap12 28511 and dfcgrg2 28851. Ideally, we would define this for functions of any set, but we will use words (see df-word 14431) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})
Theorem	iscgrg 28500*	The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ ∼ = (cgrG‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))))