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	$⊢ {Dim}_{𝒢} \geq = \{⟨g, n⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists f (f : (1 ..^n) \underset{1-1}{⟶} p \land \exists x \in p \exists y \in p \exists z \in p (\forall j \in (2 ..^n) (f (1) d x = f (j) d x \land f (1) d y = f (j) d y \land f (1) d z = f (j) d z) \land \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))\}$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-trkgld

Detailed syntax breakdown