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

Definition df-trkg 23967
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,  ( x  .-  y )  =  ( z  .-  w ) where  .-  =  ( dist `  W )
  • for betweenness,  y  e.  ( x I z ), where  I  =  (Itv `  W )
With this definition, the axiom A2 is actually equivalent to the transitivity of addition, eqtrd 2423.

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 (TarskiGBC)
  • A5 5-segment axiom (TarskiGBC)
  • A6 Identity for the betweenness relation (TarskiGB)
  • A7 Axiom of Pasch (TarskiGB)
  • A8 Lower dimension axiom (TarskiG2D)
  • A9 Upper dimension axiom (TarskiG2D)
  • 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 TarskiG2D
  • 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  i^i TarskiGB )  i^i  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
Distinct variable group:    f, p, i, x, y, z

Detailed syntax breakdown of Definition df-trkg
StepHypRef Expression
1 cstrkg 23942 . 2  class TarskiG
2 cstrkgc 23943 . . . 4  class TarskiGC
3 cstrkgb 23944 . . . 4  class TarskiGB
42, 3cin 3388 . . 3  class  (TarskiGC  i^i TarskiGB )
5 cstrkgcb 23945 . . . 4  class TarskiGCB
6 vf . . . . . . . . . 10  setvar  f
76cv 1398 . . . . . . . . 9  class  f
8 clng 23950 . . . . . . . . 9  class LineG
97, 8cfv 5496 . . . . . . . 8  class  (LineG `  f )
10 vx . . . . . . . . 9  setvar  x
11 vy . . . . . . . . 9  setvar  y
12 vp . . . . . . . . . 10  setvar  p
1312cv 1398 . . . . . . . . 9  class  p
1410cv 1398 . . . . . . . . . . 11  class  x
1514csn 3944 . . . . . . . . . 10  class  { x }
1613, 15cdif 3386 . . . . . . . . 9  class  ( p 
\  { x }
)
17 vz . . . . . . . . . . . . 13  setvar  z
1817cv 1398 . . . . . . . . . . . 12  class  z
1911cv 1398 . . . . . . . . . . . . 13  class  y
20 vi . . . . . . . . . . . . . 14  setvar  i
2120cv 1398 . . . . . . . . . . . . 13  class  i
2214, 19, 21co 6196 . . . . . . . . . . . 12  class  ( x i y )
2318, 22wcel 1826 . . . . . . . . . . 11  wff  z  e.  ( x i y )
2418, 19, 21co 6196 . . . . . . . . . . . 12  class  ( z i y )
2514, 24wcel 1826 . . . . . . . . . . 11  wff  x  e.  ( z i y )
2614, 18, 21co 6196 . . . . . . . . . . . 12  class  ( x i z )
2719, 26wcel 1826 . . . . . . . . . . 11  wff  y  e.  ( x i z )
2823, 25, 27w3o 970 . . . . . . . . . 10  wff  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
2928, 17, 13crab 2736 . . . . . . . . 9  class  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) }
3010, 11, 13, 16, 29cmpt2 6198 . . . . . . . 8  class  ( x  e.  p ,  y  e.  ( p  \  { x } ) 
|->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
319, 30wceq 1399 . . . . . . 7  wff  (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
32 citv 23949 . . . . . . . 8  class Itv
337, 32cfv 5496 . . . . . . 7  class  (Itv `  f )
3431, 20, 33wsbc 3252 . . . . . 6  wff  [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
35 cbs 14634 . . . . . . 7  class  Base
367, 35cfv 5496 . . . . . 6  class  ( Base `  f )
3734, 12, 36wsbc 3252 . . . . 5  wff  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
3837, 6cab 2367 . . . 4  class  { f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f
)  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  (
p  \  { x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) }
395, 38cin 3388 . . 3  class  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } )
404, 39cin 3388 . 2  class  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  { f  | 
[. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
411, 40wceq 1399 1  wff TarskiG  =  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
Colors of variables: wff setvar class
This definition is referenced by:  axtgcgrrflx  23976  axtgcgrid  23977  axtgsegcon  23978  axtg5seg  23979  axtgbtwnid  23980  axtgpasch  23981  axtgcont1  23982  tglng  24053  f1otrg  24295  eengtrkg  24409
  Copyright terms: Public domain W3C validator