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 DimTarskiG≥ = { ⟨ 𝑔 , 𝑛 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgld ⊢ DimTarskiG≥
1 vg ⊢ 𝑔
2 vn ⊢ 𝑛
3 cbs ⊢ Base
4 1 cv ⊢ 𝑔
5 4 3 cfv ⊢ ( Base ‘ 𝑔 )
6 vp ⊢ 𝑝
7 cds ⊢ dist
8 4 7 cfv ⊢ ( dist ‘ 𝑔 )
9 vd ⊢ 𝑑
10 citv ⊢ Itv
11 4 10 cfv ⊢ ( Itv ‘ 𝑔 )
12 vi ⊢ 𝑖
13 vf ⊢ 𝑓
14 13 cv ⊢ 𝑓
15 c1 ⊢ 1
16 cfzo ⊢ ..^
17 2 cv ⊢ 𝑛
18 15 17 16 co ⊢ ( 1 ..^ 𝑛 )
19 6 cv ⊢ 𝑝
20 18 19 14 wf1 ⊢ 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝
21 vx ⊢ 𝑥
22 vy ⊢ 𝑦
23 vz ⊢ 𝑧
24 vj ⊢ 𝑗
25 c2 ⊢ 2
26 25 17 16 co ⊢ ( 2 ..^ 𝑛 )
27 15 14 cfv ⊢ ( 𝑓 ‘ 1 )
28 9 cv ⊢ 𝑑
29 21 cv ⊢ 𝑥
30 27 29 28 co ⊢ ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 )
31 24 cv ⊢ 𝑗
32 31 14 cfv ⊢ ( 𝑓 ‘ 𝑗 )
33 32 29 28 co ⊢ ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 )
34 30 33 wceq ⊢ ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 )
35 22 cv ⊢ 𝑦
36 27 35 28 co ⊢ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 )
37 32 35 28 co ⊢ ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 )
38 36 37 wceq ⊢ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 )
39 23 cv ⊢ 𝑧
40 27 39 28 co ⊢ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 )
41 32 39 28 co ⊢ ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 )
42 40 41 wceq ⊢ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 )
43 34 38 42 w3a ⊢ ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) )
44 43 24 26 wral ⊢ ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) )
45 12 cv ⊢ 𝑖
46 29 35 45 co ⊢ ( 𝑥 𝑖 𝑦 )
47 39 46 wcel ⊢ 𝑧 ∈ ( 𝑥 𝑖 𝑦 )
48 39 35 45 co ⊢ ( 𝑧 𝑖 𝑦 )
49 29 48 wcel ⊢ 𝑥 ∈ ( 𝑧 𝑖 𝑦 )
50 29 39 45 co ⊢ ( 𝑥 𝑖 𝑧 )
51 35 50 wcel ⊢ 𝑦 ∈ ( 𝑥 𝑖 𝑧 )
52 47 49 51 w3o ⊢ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) )
53 52 wn ⊢ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) )
54 44 53 wa ⊢ ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
55 54 23 19 wrex ⊢ ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
56 55 22 19 wrex ⊢ ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
57 56 21 19 wrex ⊢ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
58 20 57 wa ⊢ ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
59 58 13 wex ⊢ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
60 59 12 11 wsbc ⊢ [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
61 60 9 8 wsbc ⊢ [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
62 61 6 5 wsbc ⊢ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
63 62 1 2 copab ⊢ { ⟨ 𝑔 , 𝑛 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) }
64 0 63 wceq ⊢ DimTarskiG≥ = { ⟨ 𝑔 , 𝑛 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑓 ( 𝑓 : ( 1 ..^ 𝑛 ) –1-1→ 𝑝 ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( ∀ 𝑗 ∈ ( 2 ..^ 𝑛 ) ( ( ( 𝑓 ‘ 1 ) 𝑑 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) 𝑑 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) 𝑑 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) }