MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-trkg Structured version   Visualization version   GIF version

Definition df-trkg 25065
Description: 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 addition, eqtrd 2639.

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.)

Assertion
Ref Expression
df-trkg TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
Distinct variable group:   𝑓,𝑝,𝑖,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkg
StepHypRef Expression
1 cstrkg 25042 . 2 class TarskiG
2 cstrkgc 25043 . . . 4 class TarskiGC
3 cstrkgb 25044 . . . 4 class TarskiGB
42, 3cin 3534 . . 3 class (TarskiGC ∩ TarskiGB)
5 cstrkgcb 25045 . . . 4 class TarskiGCB
6 vf . . . . . . . . . 10 setvar 𝑓
76cv 1473 . . . . . . . . 9 class 𝑓
8 clng 25049 . . . . . . . . 9 class LineG
97, 8cfv 5786 . . . . . . . 8 class (LineG‘𝑓)
10 vx . . . . . . . . 9 setvar 𝑥
11 vy . . . . . . . . 9 setvar 𝑦
12 vp . . . . . . . . . 10 setvar 𝑝
1312cv 1473 . . . . . . . . 9 class 𝑝
1410cv 1473 . . . . . . . . . . 11 class 𝑥
1514csn 4120 . . . . . . . . . 10 class {𝑥}
1613, 15cdif 3532 . . . . . . . . 9 class (𝑝 ∖ {𝑥})
17 vz . . . . . . . . . . . . 13 setvar 𝑧
1817cv 1473 . . . . . . . . . . . 12 class 𝑧
1911cv 1473 . . . . . . . . . . . . 13 class 𝑦
20 vi . . . . . . . . . . . . . 14 setvar 𝑖
2120cv 1473 . . . . . . . . . . . . 13 class 𝑖
2214, 19, 21co 6523 . . . . . . . . . . . 12 class (𝑥𝑖𝑦)
2318, 22wcel 1975 . . . . . . . . . . 11 wff 𝑧 ∈ (𝑥𝑖𝑦)
2418, 19, 21co 6523 . . . . . . . . . . . 12 class (𝑧𝑖𝑦)
2514, 24wcel 1975 . . . . . . . . . . 11 wff 𝑥 ∈ (𝑧𝑖𝑦)
2614, 18, 21co 6523 . . . . . . . . . . . 12 class (𝑥𝑖𝑧)
2719, 26wcel 1975 . . . . . . . . . . 11 wff 𝑦 ∈ (𝑥𝑖𝑧)
2823, 25, 27w3o 1029 . . . . . . . . . 10 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
2928, 17, 13crab 2895 . . . . . . . . 9 class {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}
3010, 11, 13, 16, 29cmpt2 6525 . . . . . . . 8 class (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
319, 30wceq 1474 . . . . . . 7 wff (LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
32 citv 25048 . . . . . . . 8 class Itv
337, 32cfv 5786 . . . . . . 7 class (Itv‘𝑓)
3431, 20, 33wsbc 3397 . . . . . 6 wff [(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
35 cbs 15637 . . . . . . 7 class Base
367, 35cfv 5786 . . . . . 6 class (Base‘𝑓)
3734, 12, 36wsbc 3397 . . . . 5 wff [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
3837, 6cab 2591 . . . 4 class {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}
395, 38cin 3534 . . 3 class (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
404, 39cin 3534 . 2 class ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
411, 40wceq 1474 1 wff TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
Colors of variables: wff setvar class
This definition is referenced by:  axtgcgrrflx  25074  axtgcgrid  25075  axtgsegcon  25076  axtg5seg  25077  axtgbtwnid  25078  axtgpasch  25079  axtgcont1  25080  tglng  25155  f1otrg  25465  eengtrkg  25579
  Copyright terms: Public domain W3C validator