Metamath Proof Explorer

Definition df-trkg

Description: Define the class of Tarski geometries. A Tarski geometry is a set of points, equipped with a betweenness relation (denoting that a point lies on a line segment between two other points) and a congruence relation (denoting equality of line segment lengths).

Here, we are using the following:

With this definition, the axiom A2 is actually equivalent to the transitivity of equality, eqtrd .

Tarski originally had more axioms, but later reduced his list to 11:

Our definition is split into 5 parts:

So our definition of a Tarskian Geometry includes the 3 axioms for the quaternary congruence relation (A1, A2, A3), the 3 axioms for the ternary betweenness relation (A6, A7, A11), and the 2 axioms of compatibility of the congruence and the betweenness relations (A4,A5).

It does not include Euclid's axiom A10, nor the 2-dimensional axioms A8 (Lower dimension axiom) and A9 (Upper dimension axiom) so the number of dimensions of the geometry it formalizes is not constrained.

Considering A2 as one of the 3 axioms for the quaternary congruence relation is somewhat conventional, because the transitivity of the congruence relation is automatically given by our choice to take the distance as this congruence relation in our definition of Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017) (Revised by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Assertion df-trkg ⊢ 𝒢 Tarski = 𝒢 Tarski C ∩ 𝒢 Tarski B ∩ 𝒢 Tarski CB ∩ f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkg class 𝒢 Tarski
1 cstrkgc class 𝒢 Tarski C
2 cstrkgb class 𝒢 Tarski B
3 1 2 cin class 𝒢 Tarski C ∩ 𝒢 Tarski B
4 cstrkgcb class 𝒢 Tarski CB
5 vf setvar f
6 cbs class Base
7 5 cv setvar f
8 7 6 cfv class Base f
9 vp setvar p
10 citv class Itv
11 7 10 cfv class Itv ⁡ f
12 vi setvar i
13 clng class Line 𝒢
14 7 13 cfv class Line 𝒢 ⁡ f
15 vx setvar x
16 9 cv setvar p
17 vy setvar y
18 15 cv setvar x
19 18 csn class x
20 16 19 cdif class p ∖ x
21 vz setvar z
22 21 cv setvar z
23 12 cv setvar i
24 17 cv setvar y
25 18 24 23 co class x i y
26 22 25 wcel wff z ∈ x i y
27 22 24 23 co class z i y
28 18 27 wcel wff x ∈ z i y
29 18 22 23 co class x i z
30 24 29 wcel wff y ∈ x i z
31 26 28 30 w3o wff z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
32 31 21 16 crab class z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
33 15 17 16 20 32 cmpo class x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
34 14 33 wceq wff Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
35 34 12 11 wsbc wff [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
36 35 9 8 wsbc wff [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
37 36 5 cab class f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
38 4 37 cin class 𝒢 Tarski CB ∩ f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
39 3 38 cin class 𝒢 Tarski C ∩ 𝒢 Tarski B ∩ 𝒢 Tarski CB ∩ f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
40 0 39 wceq wff 𝒢 Tarski = 𝒢 Tarski C ∩ 𝒢 Tarski B ∩ 𝒢 Tarski CB ∩ f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z