Metamath Proof Explorer

Theorem istrkgc

Description: Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses istrkg.p 
|- P = ( Base ` G )
istrkg.d 
|- .- = ( dist ` G )
istrkg.i 
|- I = ( Itv ` G )
Assertion istrkgc 
|- ( G e. TarskiGC <-> ( G e. _V /\ ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p 
 |-  P = ( Base ` G )
2 istrkg.d 
 |-  .- = ( dist ` G )
3 istrkg.i 
 |-  I = ( Itv ` G )
4 simpl 
 |-  ( ( p = P /\ d = .- ) -> p = P )
5 simpr 
 |-  ( ( p = P /\ d = .- ) -> d = .- )
6 5 oveqd 
 |-  ( ( p = P /\ d = .- ) -> ( x d y ) = ( x .- y ) )
7 5 oveqd 
 |-  ( ( p = P /\ d = .- ) -> ( y d x ) = ( y .- x ) )
8 6 7 eqeq12d 
 |-  ( ( p = P /\ d = .- ) -> ( ( x d y ) = ( y d x ) <-> ( x .- y ) = ( y .- x ) ) )
9 4 8 raleqbidv 
 |-  ( ( p = P /\ d = .- ) -> ( A. y e. p ( x d y ) = ( y d x ) <-> A. y e. P ( x .- y ) = ( y .- x ) ) )
10 4 9 raleqbidv 
 |-  ( ( p = P /\ d = .- ) -> ( A. x e. p A. y e. p ( x d y ) = ( y d x ) <-> A. x e. P A. y e. P ( x .- y ) = ( y .- x ) ) )
11 5 oveqd 
 |-  ( ( p = P /\ d = .- ) -> ( z d z ) = ( z .- z ) )
12 6 11 eqeq12d 
 |-  ( ( p = P /\ d = .- ) -> ( ( x d y ) = ( z d z ) <-> ( x .- y ) = ( z .- z ) ) )
13 12 imbi1d 
 |-  ( ( p = P /\ d = .- ) -> ( ( ( x d y ) = ( z d z ) -> x = y ) <-> ( ( x .- y ) = ( z .- z ) -> x = y ) ) )
14 4 13 raleqbidv 
 |-  ( ( p = P /\ d = .- ) -> ( A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) <-> A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) )
15 4 14 raleqbidv 
 |-  ( ( p = P /\ d = .- ) -> ( A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) <-> A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) )
16 4 15 raleqbidv 
 |-  ( ( p = P /\ d = .- ) -> ( A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) <-> A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) )
17 10 16 anbi12d 
 |-  ( ( p = P /\ 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 ) ) <-> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) ) )
18 1 2 17 sbcie2s 
 |-  ( f = G -> ( [. ( 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 ) ) <-> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) ) )
19 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 ) ) }
20 18 19 elab4g 
 |-  ( G e. TarskiGC <-> ( G e. _V /\ ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) ) )