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

Definition df-trkgld 24579
Description: Define the class of geometries fulfilling the lower dimension axiom for dimension  n. For such geometries, there are three non-colinear points that are equidistant from  n  -  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.)
Assertion
Ref Expression
df-trkgld  |- DimTarskiG =  { <. g ,  n >.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g )  /  d ]. [. (Itv `  g
)  /  i ]. E. f ( f : ( 1..^ n )
-1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  ( 2..^ n ) ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) ) }
Distinct variable group:    f, d, g, n, p, i, j, x, y, z

Detailed syntax breakdown of Definition df-trkgld
StepHypRef Expression
1 cstrkgld 24561 . 2  class DimTarskiG
2 c1 9558 . . . . . . . . . 10  class  1
3 vn . . . . . . . . . . 11  setvar  n
43cv 1451 . . . . . . . . . 10  class  n
5 cfzo 11942 . . . . . . . . . 10  class ..^
62, 4, 5co 6308 . . . . . . . . 9  class  ( 1..^ n )
7 vp . . . . . . . . . 10  setvar  p
87cv 1451 . . . . . . . . 9  class  p
9 vf . . . . . . . . . 10  setvar  f
109cv 1451 . . . . . . . . 9  class  f
116, 8, 10wf1 5586 . . . . . . . 8  wff  f : ( 1..^ n )
-1-1-> p
122, 10cfv 5589 . . . . . . . . . . . . . . . 16  class  ( f `
 1 )
13 vx . . . . . . . . . . . . . . . . 17  setvar  x
1413cv 1451 . . . . . . . . . . . . . . . 16  class  x
15 vd . . . . . . . . . . . . . . . . 17  setvar  d
1615cv 1451 . . . . . . . . . . . . . . . 16  class  d
1712, 14, 16co 6308 . . . . . . . . . . . . . . 15  class  ( ( f `  1 ) d x )
18 vj . . . . . . . . . . . . . . . . . 18  setvar  j
1918cv 1451 . . . . . . . . . . . . . . . . 17  class  j
2019, 10cfv 5589 . . . . . . . . . . . . . . . 16  class  ( f `
 j )
2120, 14, 16co 6308 . . . . . . . . . . . . . . 15  class  ( ( f `  j ) d x )
2217, 21wceq 1452 . . . . . . . . . . . . . 14  wff  ( ( f `  1 ) d x )  =  ( ( f `  j ) d x )
23 vy . . . . . . . . . . . . . . . . 17  setvar  y
2423cv 1451 . . . . . . . . . . . . . . . 16  class  y
2512, 24, 16co 6308 . . . . . . . . . . . . . . 15  class  ( ( f `  1 ) d y )
2620, 24, 16co 6308 . . . . . . . . . . . . . . 15  class  ( ( f `  j ) d y )
2725, 26wceq 1452 . . . . . . . . . . . . . 14  wff  ( ( f `  1 ) d y )  =  ( ( f `  j ) d y )
28 vz . . . . . . . . . . . . . . . . 17  setvar  z
2928cv 1451 . . . . . . . . . . . . . . . 16  class  z
3012, 29, 16co 6308 . . . . . . . . . . . . . . 15  class  ( ( f `  1 ) d z )
3120, 29, 16co 6308 . . . . . . . . . . . . . . 15  class  ( ( f `  j ) d z )
3230, 31wceq 1452 . . . . . . . . . . . . . 14  wff  ( ( f `  1 ) d z )  =  ( ( f `  j ) d z )
3322, 27, 32w3a 1007 . . . . . . . . . . . . 13  wff  ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )
34 c2 10681 . . . . . . . . . . . . . 14  class  2
3534, 4, 5co 6308 . . . . . . . . . . . . 13  class  ( 2..^ n )
3633, 18, 35wral 2756 . . . . . . . . . . . 12  wff  A. j  e.  ( 2..^ n ) ( ( ( f `
 1 ) d x )  =  ( ( f `  j
) d x )  /\  ( ( f `
 1 ) d y )  =  ( ( f `  j
) d y )  /\  ( ( f `
 1 ) d z )  =  ( ( f `  j
) d z ) )
37 vi . . . . . . . . . . . . . . . . 17  setvar  i
3837cv 1451 . . . . . . . . . . . . . . . 16  class  i
3914, 24, 38co 6308 . . . . . . . . . . . . . . 15  class  ( x i y )
4029, 39wcel 1904 . . . . . . . . . . . . . 14  wff  z  e.  ( x i y )
4129, 24, 38co 6308 . . . . . . . . . . . . . . 15  class  ( z i y )
4214, 41wcel 1904 . . . . . . . . . . . . . 14  wff  x  e.  ( z i y )
4314, 29, 38co 6308 . . . . . . . . . . . . . . 15  class  ( x i z )
4424, 43wcel 1904 . . . . . . . . . . . . . 14  wff  y  e.  ( x i z )
4540, 42, 44w3o 1006 . . . . . . . . . . . . 13  wff  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
4645wn 3 . . . . . . . . . . . 12  wff  -.  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
4736, 46wa 376 . . . . . . . . . . 11  wff  ( A. j  e.  ( 2..^ n ) ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4847, 28, 8wrex 2757 . . . . . . . . . 10  wff  E. z  e.  p  ( A. j  e.  ( 2..^ n ) ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4948, 23, 8wrex 2757 . . . . . . . . 9  wff  E. y  e.  p  E. z  e.  p  ( A. j  e.  ( 2..^ n ) ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
5049, 13, 8wrex 2757 . . . . . . . 8  wff  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  ( 2..^ n ) ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
5111, 50wa 376 . . . . . . 7  wff  ( f : ( 1..^ n ) -1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  (
2..^ n ) ( ( ( f ` 
1 ) d x )  =  ( ( f `  j ) d x )  /\  ( ( f ` 
1 ) d y )  =  ( ( f `  j ) d y )  /\  ( ( f ` 
1 ) d z )  =  ( ( f `  j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
5251, 9wex 1671 . . . . . 6  wff  E. f
( f : ( 1..^ n ) -1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  ( 2..^ n ) ( ( ( f ` 
1 ) d x )  =  ( ( f `  j ) d x )  /\  ( ( f ` 
1 ) d y )  =  ( ( f `  j ) d y )  /\  ( ( f ` 
1 ) d z )  =  ( ( f `  j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
53 vg . . . . . . . 8  setvar  g
5453cv 1451 . . . . . . 7  class  g
55 citv 24563 . . . . . . 7  class Itv
5654, 55cfv 5589 . . . . . 6  class  (Itv `  g )
5752, 37, 56wsbc 3255 . . . . 5  wff  [. (Itv `  g )  /  i ]. E. f ( f : ( 1..^ n ) -1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  (
2..^ n ) ( ( ( f ` 
1 ) d x )  =  ( ( f `  j ) d x )  /\  ( ( f ` 
1 ) d y )  =  ( ( f `  j ) d y )  /\  ( ( f ` 
1 ) d z )  =  ( ( f `  j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
58 cds 15277 . . . . . 6  class  dist
5954, 58cfv 5589 . . . . 5  class  ( dist `  g )
6057, 15, 59wsbc 3255 . . . 4  wff  [. ( dist `  g )  / 
d ]. [. (Itv `  g )  /  i ]. E. f ( f : ( 1..^ n ) -1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  (
2..^ n ) ( ( ( f ` 
1 ) d x )  =  ( ( f `  j ) d x )  /\  ( ( f ` 
1 ) d y )  =  ( ( f `  j ) d y )  /\  ( ( f ` 
1 ) d z )  =  ( ( f `  j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
61 cbs 15199 . . . . 5  class  Base
6254, 61cfv 5589 . . . 4  class  ( Base `  g )
6360, 7, 62wsbc 3255 . . 3  wff  [. ( Base `  g )  /  p ]. [. ( dist `  g )  /  d ]. [. (Itv `  g
)  /  i ]. E. f ( f : ( 1..^ n )
-1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  ( 2..^ n ) ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
6463, 53, 3copab 4453 . 2  class  { <. g ,  n >.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g )  / 
d ]. [. (Itv `  g )  /  i ]. E. f ( f : ( 1..^ n ) -1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  (
2..^ n ) ( ( ( f ` 
1 ) d x )  =  ( ( f `  j ) d x )  /\  ( ( f ` 
1 ) d y )  =  ( ( f `  j ) d y )  /\  ( ( f ` 
1 ) d z )  =  ( ( f `  j ) d z ) )  /\  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) ) }
651, 64wceq 1452 1  wff DimTarskiG =  { <. g ,  n >.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g )  /  d ]. [. (Itv `  g
)  /  i ]. E. f ( f : ( 1..^ n )
-1-1-> p  /\  E. x  e.  p  E. y  e.  p  E. z  e.  p  ( A. j  e.  ( 2..^ n ) ( ( ( f `  1
) d x )  =  ( ( f `
 j ) d x )  /\  (
( f `  1
) d y )  =  ( ( f `
 j ) d y )  /\  (
( f `  1
) d z )  =  ( ( f `
 j ) d z ) )  /\  -.  ( 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:  istrkgld  24586
  Copyright terms: Public domain W3C validator