Metamath Proof Explorer

Definition df-trkgc

Description: Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of Schwabhauser p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr , so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017)

Ref Expression
Assertion df-trkgc 
|- TarskiGC = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgc 
 |-  TarskiGC
1 vf 
 |-  f
2 cbs 
 |-  Base
3 1 cv 
 |-  f
4 3 2 cfv 
 |-  ( Base ` f )
5 vp 
 |-  p
6 cds 
 |-  dist
7 3 6 cfv 
 |-  ( dist ` f )
8 vd 
 |-  d
9 vx 
 |-  x
10 5 cv 
 |-  p
11 vy 
 |-  y
12 9 cv 
 |-  x
13 8 cv 
 |-  d
14 11 cv 
 |-  y
15 12 14 13 co 
 |-  ( x d y )
16 14 12 13 co 
 |-  ( y d x )
17 15 16 wceq 
 |-  ( x d y ) = ( y d x )
18 17 11 10 wral 
 |-  A. y e. p ( x d y ) = ( y d x )
19 18 9 10 wral 
 |-  A. x e. p A. y e. p ( x d y ) = ( y d x )
20 vz 
 |-  z
21 20 cv 
 |-  z
22 21 21 13 co 
 |-  ( z d z )
23 15 22 wceq 
 |-  ( x d y ) = ( z d z )
24 12 14 wceq 
 |-  x = y
25 23 24 wi 
 |-  ( ( x d y ) = ( z d z ) -> x = y )
26 25 20 10 wral 
 |-  A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
27 26 11 10 wral 
 |-  A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
28 27 9 10 wral 
 |-  A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
29 19 28 wa 
 |-  ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) )
30 29 8 7 wsbc 
 |-  [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) )
31 30 5 4 wsbc 
 |-  [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) )
32 31 1 cab 
 |-  { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) }
33 0 32 wceq 
 |-  TarskiGC = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) }