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 27971
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 27950 . 2 class DimTarskiGβ‰₯
2 c1 11115 . . . . . . . . . 10 class 1
3 vn . . . . . . . . . . 11 setvar 𝑛
43cv 1539 . . . . . . . . . 10 class 𝑛
5 cfzo 13632 . . . . . . . . . 10 class ..^
62, 4, 5co 7412 . . . . . . . . 9 class (1..^𝑛)
7 vp . . . . . . . . . 10 setvar 𝑝
87cv 1539 . . . . . . . . 9 class 𝑝
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1539 . . . . . . . . 9 class 𝑓
116, 8, 10wf1 6540 . . . . . . . 8 wff 𝑓:(1..^𝑛)–1-1→𝑝
122, 10cfv 6543 . . . . . . . . . . . . . . . 16 class (π‘“β€˜1)
13 vx . . . . . . . . . . . . . . . . 17 setvar π‘₯
1413cv 1539 . . . . . . . . . . . . . . . 16 class π‘₯
15 vd . . . . . . . . . . . . . . . . 17 setvar 𝑑
1615cv 1539 . . . . . . . . . . . . . . . 16 class 𝑑
1712, 14, 16co 7412 . . . . . . . . . . . . . . 15 class ((π‘“β€˜1)𝑑π‘₯)
18 vj . . . . . . . . . . . . . . . . . 18 setvar 𝑗
1918cv 1539 . . . . . . . . . . . . . . . . 17 class 𝑗
2019, 10cfv 6543 . . . . . . . . . . . . . . . 16 class (π‘“β€˜π‘—)
2120, 14, 16co 7412 . . . . . . . . . . . . . . 15 class ((π‘“β€˜π‘—)𝑑π‘₯)
2217, 21wceq 1540 . . . . . . . . . . . . . 14 wff ((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯)
23 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
2423cv 1539 . . . . . . . . . . . . . . . 16 class 𝑦
2512, 24, 16co 7412 . . . . . . . . . . . . . . 15 class ((π‘“β€˜1)𝑑𝑦)
2620, 24, 16co 7412 . . . . . . . . . . . . . . 15 class ((π‘“β€˜π‘—)𝑑𝑦)
2725, 26wceq 1540 . . . . . . . . . . . . . 14 wff ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦)
28 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
2928cv 1539 . . . . . . . . . . . . . . . 16 class 𝑧
3012, 29, 16co 7412 . . . . . . . . . . . . . . 15 class ((π‘“β€˜1)𝑑𝑧)
3120, 29, 16co 7412 . . . . . . . . . . . . . . 15 class ((π‘“β€˜π‘—)𝑑𝑧)
3230, 31wceq 1540 . . . . . . . . . . . . . 14 wff ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)
3322, 27, 32w3a 1086 . . . . . . . . . . . . 13 wff (((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧))
34 c2 12272 . . . . . . . . . . . . . 14 class 2
3534, 4, 5co 7412 . . . . . . . . . . . . 13 class (2..^𝑛)
3633, 18, 35wral 3060 . . . . . . . . . . . 12 wff βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧))
37 vi . . . . . . . . . . . . . . . . 17 setvar 𝑖
3837cv 1539 . . . . . . . . . . . . . . . 16 class 𝑖
3914, 24, 38co 7412 . . . . . . . . . . . . . . 15 class (π‘₯𝑖𝑦)
4029, 39wcel 2105 . . . . . . . . . . . . . 14 wff 𝑧 ∈ (π‘₯𝑖𝑦)
4129, 24, 38co 7412 . . . . . . . . . . . . . . 15 class (𝑧𝑖𝑦)
4214, 41wcel 2105 . . . . . . . . . . . . . 14 wff π‘₯ ∈ (𝑧𝑖𝑦)
4314, 29, 38co 7412 . . . . . . . . . . . . . . 15 class (π‘₯𝑖𝑧)
4424, 43wcel 2105 . . . . . . . . . . . . . 14 wff 𝑦 ∈ (π‘₯𝑖𝑧)
4540, 42, 44w3o 1085 . . . . . . . . . . . . 13 wff (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
4645wn 3 . . . . . . . . . . . 12 wff Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
4736, 46wa 395 . . . . . . . . . . 11 wff (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4847, 28, 8wrex 3069 . . . . . . . . . 10 wff βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4948, 23, 8wrex 3069 . . . . . . . . 9 wff βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
5049, 13, 8wrex 3069 . . . . . . . 8 wff βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
5111, 50wa 395 . . . . . . 7 wff (𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
5251, 9wex 1780 . . . . . 6 wff βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
53 vg . . . . . . . 8 setvar 𝑔
5453cv 1539 . . . . . . 7 class 𝑔
55 citv 27952 . . . . . . 7 class Itv
5654, 55cfv 6543 . . . . . 6 class (Itvβ€˜π‘”)
5752, 37, 56wsbc 3777 . . . . 5 wff [(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
58 cds 17211 . . . . . 6 class dist
5954, 58cfv 6543 . . . . 5 class (distβ€˜π‘”)
6057, 15, 59wsbc 3777 . . . 4 wff [(distβ€˜π‘”) / 𝑑][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
61 cbs 17149 . . . . 5 class Base
6254, 61cfv 6543 . . . 4 class (Baseβ€˜π‘”)
6360, 7, 62wsbc 3777 . . 3 wff [(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / 𝑑][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
6463, 53, 3copab 5210 . 2 class {βŸ¨π‘”, π‘›βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / 𝑑][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘“(𝑓:(1..^𝑛)–1-1→𝑝 ∧ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 (βˆ€π‘— ∈ (2..^𝑛)(((π‘“β€˜1)𝑑π‘₯) = ((π‘“β€˜π‘—)𝑑π‘₯) ∧ ((π‘“β€˜1)𝑑𝑦) = ((π‘“β€˜π‘—)𝑑𝑦) ∧ ((π‘“β€˜1)𝑑𝑧) = ((π‘“β€˜π‘—)𝑑𝑧)) ∧ Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))}
651, 64wceq 1540 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  27978
  Copyright terms: Public domain W3C validator