Definition df-trkgld 25351

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

Step	Hyp	Ref	Expression
1		cstrkgld 25333	. 2 class DimTarskiG≥
2		c1 9937	. . . . . . . . . 10 class 1
3		vn	. . . . . . . . . . 11 setvar n
4	3	cv 1482	. . . . . . . . . 10 class n
5		cfzo 12465	. . . . . . . . . 10 class ..^
6	2, 4, 5	co 6650	. . . . . . . . 9 class ( 1..^ n )
7		vp	. . . . . . . . . 10 setvar p
8	7	cv 1482	. . . . . . . . 9 class p
9		vf	. . . . . . . . . 10 setvar f
10	9	cv 1482	. . . . . . . . 9 class f
11	6, 8, 10	wf1 5885	. . . . . . . 8 wff f : ( 1..^ n ) -1-1-> p
12	2, 10	cfv 5888	. . . . . . . . . . . . . . . 16 class ( f ` 1 )
13		vx	. . . . . . . . . . . . . . . . 17 setvar x
14	13	cv 1482	. . . . . . . . . . . . . . . 16 class x
15		vd	. . . . . . . . . . . . . . . . 17 setvar d
16	15	cv 1482	. . . . . . . . . . . . . . . 16 class d
17	12, 14, 16	co 6650	. . . . . . . . . . . . . . 15 class ( ( f ` 1 ) d x )
18		vj	. . . . . . . . . . . . . . . . . 18 setvar j
19	18	cv 1482	. . . . . . . . . . . . . . . . 17 class j
20	19, 10	cfv 5888	. . . . . . . . . . . . . . . 16 class ( f ` j )
21	20, 14, 16	co 6650	. . . . . . . . . . . . . . 15 class ( ( f ` j ) d x )
22	17, 21	wceq 1483	. . . . . . . . . . . . . 14 wff ( ( f ` 1 ) d x ) = ( ( f ` j ) d x )
23		vy	. . . . . . . . . . . . . . . . 17 setvar y
24	23	cv 1482	. . . . . . . . . . . . . . . 16 class y
25	12, 24, 16	co 6650	. . . . . . . . . . . . . . 15 class ( ( f ` 1 ) d y )
26	20, 24, 16	co 6650	. . . . . . . . . . . . . . 15 class ( ( f ` j ) d y )
27	25, 26	wceq 1483	. . . . . . . . . . . . . 14 wff ( ( f ` 1 ) d y ) = ( ( f ` j ) d y )
28		vz	. . . . . . . . . . . . . . . . 17 setvar z
29	28	cv 1482	. . . . . . . . . . . . . . . 16 class z
30	12, 29, 16	co 6650	. . . . . . . . . . . . . . 15 class ( ( f ` 1 ) d z )
31	20, 29, 16	co 6650	. . . . . . . . . . . . . . 15 class ( ( f ` j ) d z )
32	30, 31	wceq 1483	. . . . . . . . . . . . . 14 wff ( ( f ` 1 ) d z ) = ( ( f ` j ) d z )
33	22, 27, 32	w3a 1037	. . . . . . . . . . . . 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 11070	. . . . . . . . . . . . . 14 class 2
35	34, 4, 5	co 6650	. . . . . . . . . . . . 13 class ( 2..^ n )
36	33, 18, 35	wral 2912	. . . . . . . . . . . 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
38	37	cv 1482	. . . . . . . . . . . . . . . 16 class i
39	14, 24, 38	co 6650	. . . . . . . . . . . . . . 15 class ( x i y )
40	29, 39	wcel 1990	. . . . . . . . . . . . . 14 wff z e. ( x i y )
41	29, 24, 38	co 6650	. . . . . . . . . . . . . . 15 class ( z i y )
42	14, 41	wcel 1990	. . . . . . . . . . . . . 14 wff x e. ( z i y )
43	14, 29, 38	co 6650	. . . . . . . . . . . . . . 15 class ( x i z )
44	24, 43	wcel 1990	. . . . . . . . . . . . . 14 wff y e. ( x i z )
45	40, 42, 44	w3o 1036	. . . . . . . . . . . . 13 wff ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
46	45	wn 3	. . . . . . . . . . . 12 wff -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
47	36, 46	wa 384	. . . . . . . . . . 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 ) ) )
48	47, 28, 8	wrex 2913	. . . . . . . . . 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 ) ) )
49	48, 23, 8	wrex 2913	. . . . . . . . 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 ) ) )
50	49, 13, 8	wrex 2913	. . . . . . . 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 ) ) )
51	11, 50	wa 384	. . . . . . 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 ) ) ) )
52	51, 9	wex 1704	. . . . . 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
54	53	cv 1482	. . . . . . 7 class g
55		citv 25335	. . . . . . 7 class Itv
56	54, 55	cfv 5888	. . . . . 6 class (Itv ` g )
57	52, 37, 56	wsbc 3435	. . . . 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 15950	. . . . . 6 class dist
59	54, 58	cfv 5888	. . . . 5 class ( dist ` g )
60	57, 15, 59	wsbc 3435	. . . 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 15857	. . . . 5 class Base
62	54, 61	cfv 5888	. . . 4 class ( Base ` g )
63	60, 7, 62	wsbc 3435	. . 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 ) ) ) )
64	63, 53, 3	copab 4712	. 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 ) ) ) ) }
65	1, 64	wceq 1483	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 ) ) ) ) }

This definition is referenced by:  istrkgld  25358