Metamath Proof Explorer

Definition df-trkgld

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 inTarski'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)

Ref Expression
Assertion df-trkgld 
|- TarskiGDim>= = { <. 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 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgld 
 |-  TarskiGDim>=
1 vg 
 |-  g
2 vn 
 |-  n
3 cbs 
 |-  Base
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Base ` g )
6 vp 
 |-  p
7 cds 
 |-  dist
8 4 7 cfv 
 |-  ( dist ` g )
9 vd 
 |-  d
10 citv 
 |-  Itv
11 4 10 cfv 
 |-  ( Itv ` g )
12 vi 
 |-  i
13 vf 
 |-  f
14 13 cv 
 |-  f
15 c1 
 |-  1
16 cfzo 
 |-  ..^
17 2 cv 
 |-  n
18 15 17 16 co 
 |-  ( 1 ..^ n )
19 6 cv 
 |-  p
20 18 19 14 wf1 
 |-  f : ( 1 ..^ n ) -1-1-> p
21 vx 
 |-  x
22 vy 
 |-  y
23 vz 
 |-  z
24 vj 
 |-  j
25 c2 
 |-  2
26 25 17 16 co 
 |-  ( 2 ..^ n )
27 15 14 cfv 
 |-  ( f ` 1 )
28 9 cv 
 |-  d
29 21 cv 
 |-  x
30 27 29 28 co 
 |-  ( ( f ` 1 ) d x )
31 24 cv 
 |-  j
32 31 14 cfv 
 |-  ( f ` j )
33 32 29 28 co 
 |-  ( ( f ` j ) d x )
34 30 33 wceq 
 |-  ( ( f ` 1 ) d x ) = ( ( f ` j ) d x )
35 22 cv 
 |-  y
36 27 35 28 co 
 |-  ( ( f ` 1 ) d y )
37 32 35 28 co 
 |-  ( ( f ` j ) d y )
38 36 37 wceq 
 |-  ( ( f ` 1 ) d y ) = ( ( f ` j ) d y )
39 23 cv 
 |-  z
40 27 39 28 co 
 |-  ( ( f ` 1 ) d z )
41 32 39 28 co 
 |-  ( ( f ` j ) d z )
42 40 41 wceq 
 |-  ( ( f ` 1 ) d z ) = ( ( f ` j ) d z )
43 34 38 42 w3a 
 |-  ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) )
44 43 24 26 wral 
 |-  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 ) )
45 12 cv 
 |-  i
46 29 35 45 co 
 |-  ( x i y )
47 39 46 wcel 
 |-  z e. ( x i y )
48 39 35 45 co 
 |-  ( z i y )
49 29 48 wcel 
 |-  x e. ( z i y )
50 29 39 45 co 
 |-  ( x i z )
51 35 50 wcel 
 |-  y e. ( x i z )
52 47 49 51 w3o 
 |-  ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
53 52 wn 
 |-  -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
54 44 53 wa 
 |-  ( 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 ) ) )
55 54 23 19 wrex 
 |-  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 ) ) )
56 55 22 19 wrex 
 |-  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 ) ) )
57 56 21 19 wrex 
 |-  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 20 57 wa 
 |-  ( 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 ) ) ) )
59 58 13 wex 
 |-  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 ) ) ) )
60 59 12 11 wsbc 
 |-  [. ( 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 60 9 8 wsbc 
 |-  [. ( 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 ) ) ) )
62 61 6 5 wsbc 
 |-  [. ( 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 ) ) ) )
63 62 1 2 copab 
 |-  { <. 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 ) ) ) ) }
64 0 63 wceq 
 |-  TarskiGDim>= = { <. 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 ) ) ) ) }