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

Definition df-trkgld 26543
Description: Define the class of geometries fulfilling the lower dimension axiom for dimension 𝑛. For such geometries, there are three non-colinear points that are equidistant from 𝑛 − 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≥ = {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
Distinct variable group:   𝑓,𝑑,𝑔,𝑛,𝑝,𝑖,𝑗,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkgld
StepHypRef Expression
1 cstrkgld 26525 . 2 class DimTarskiG
2 c1 10730 . . . . . . . . . 10 class 1
3 vn . . . . . . . . . . 11 setvar 𝑛
43cv 1542 . . . . . . . . . 10 class 𝑛
5 cfzo 13238 . . . . . . . . . 10 class ..^
62, 4, 5co 7213 . . . . . . . . 9 class (1..^𝑛)
7 vp . . . . . . . . . 10 setvar 𝑝
87cv 1542 . . . . . . . . 9 class 𝑝
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1542 . . . . . . . . 9 class 𝑓
116, 8, 10wf1 6377 . . . . . . . 8 wff 𝑓:(1..^𝑛)–1-1𝑝
122, 10cfv 6380 . . . . . . . . . . . . . . . 16 class (𝑓‘1)
13 vx . . . . . . . . . . . . . . . . 17 setvar 𝑥
1413cv 1542 . . . . . . . . . . . . . . . 16 class 𝑥
15 vd . . . . . . . . . . . . . . . . 17 setvar 𝑑
1615cv 1542 . . . . . . . . . . . . . . . 16 class 𝑑
1712, 14, 16co 7213 . . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑥)
18 vj . . . . . . . . . . . . . . . . . 18 setvar 𝑗
1918cv 1542 . . . . . . . . . . . . . . . . 17 class 𝑗
2019, 10cfv 6380 . . . . . . . . . . . . . . . 16 class (𝑓𝑗)
2120, 14, 16co 7213 . . . . . . . . . . . . . . 15 class ((𝑓𝑗)𝑑𝑥)
2217, 21wceq 1543 . . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥)
23 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
2423cv 1542 . . . . . . . . . . . . . . . 16 class 𝑦
2512, 24, 16co 7213 . . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑦)
2620, 24, 16co 7213 . . . . . . . . . . . . . . 15 class ((𝑓𝑗)𝑑𝑦)
2725, 26wceq 1543 . . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦)
28 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
2928cv 1542 . . . . . . . . . . . . . . . 16 class 𝑧
3012, 29, 16co 7213 . . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑧)
3120, 29, 16co 7213 . . . . . . . . . . . . . . 15 class ((𝑓𝑗)𝑑𝑧)
3230, 31wceq 1543 . . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)
3322, 27, 32w3a 1089 . . . . . . . . . . . . 13 wff (((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧))
34 c2 11885 . . . . . . . . . . . . . 14 class 2
3534, 4, 5co 7213 . . . . . . . . . . . . 13 class (2..^𝑛)
3633, 18, 35wral 3061 . . . . . . . . . . . 12 wff 𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧))
37 vi . . . . . . . . . . . . . . . . 17 setvar 𝑖
3837cv 1542 . . . . . . . . . . . . . . . 16 class 𝑖
3914, 24, 38co 7213 . . . . . . . . . . . . . . 15 class (𝑥𝑖𝑦)
4029, 39wcel 2110 . . . . . . . . . . . . . 14 wff 𝑧 ∈ (𝑥𝑖𝑦)
4129, 24, 38co 7213 . . . . . . . . . . . . . . 15 class (𝑧𝑖𝑦)
4214, 41wcel 2110 . . . . . . . . . . . . . 14 wff 𝑥 ∈ (𝑧𝑖𝑦)
4314, 29, 38co 7213 . . . . . . . . . . . . . . 15 class (𝑥𝑖𝑧)
4424, 43wcel 2110 . . . . . . . . . . . . . 14 wff 𝑦 ∈ (𝑥𝑖𝑧)
4540, 42, 44w3o 1088 . . . . . . . . . . . . 13 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4645wn 3 . . . . . . . . . . . 12 wff ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4736, 46wa 399 . . . . . . . . . . 11 wff (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4847, 28, 8wrex 3062 . . . . . . . . . 10 wff 𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4948, 23, 8wrex 3062 . . . . . . . . 9 wff 𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
5049, 13, 8wrex 3062 . . . . . . . 8 wff 𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
5111, 50wa 399 . . . . . . 7 wff (𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
5251, 9wex 1787 . . . . . 6 wff 𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
53 vg . . . . . . . 8 setvar 𝑔
5453cv 1542 . . . . . . 7 class 𝑔
55 citv 26527 . . . . . . 7 class Itv
5654, 55cfv 6380 . . . . . 6 class (Itv‘𝑔)
5752, 37, 56wsbc 3694 . . . . 5 wff [(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
58 cds 16811 . . . . . 6 class dist
5954, 58cfv 6380 . . . . 5 class (dist‘𝑔)
6057, 15, 59wsbc 3694 . . . 4 wff [(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
61 cbs 16760 . . . . 5 class Base
6254, 61cfv 6380 . . . 4 class (Base‘𝑔)
6360, 7, 62wsbc 3694 . . 3 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
6463, 53, 3copab 5115 . 2 class {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
651, 64wceq 1543 1 wff DimTarskiG≥ = {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkgld  26550
  Copyright terms: Public domain W3C validator