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 4 eqcomd 
 |-  ( ( p = P /\ d = .- ) -> P = p )
6 5 adantr 
 |-  ( ( ( p = P /\ d = .- ) /\ x e. P ) -> P = p )
7 simpllr 
 |-  ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) -> d = .- )
8 7 eqcomd 
 |-  ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) -> .- = d )
9 8 oveqd 
 |-  ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) -> ( x .- y ) = ( x d y ) )
10 8 oveqd 
 |-  ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) -> ( y .- x ) = ( y d x ) )
11 9 10 eqeq12d 
 |-  ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) -> ( ( x .- y ) = ( y .- x ) <-> ( x d y ) = ( y d x ) ) )
12 6 11 raleqbidva 
 |-  ( ( ( p = P /\ d = .- ) /\ x e. P ) -> ( A. y e. P ( x .- y ) = ( y .- x ) <-> A. y e. p ( x d y ) = ( y d x ) ) )
13 5 12 raleqbidva 
 |-  ( ( p = P /\ d = .- ) -> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) <-> A. x e. p A. y e. p ( x d y ) = ( y d x ) ) )
14 6 adantr 
 |-  ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) -> P = p )
15 8 oveqdr 
 |-  ( ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( x .- y ) = ( x d y ) )
16 8 oveqdr 
 |-  ( ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( z .- z ) = ( z d z ) )
17 15 16 eqeq12d 
 |-  ( ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( ( x .- y ) = ( z .- z ) <-> ( x d y ) = ( z d z ) ) )
18 17 imbi1d 
 |-  ( ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( ( ( x .- y ) = ( z .- z ) -> x = y ) <-> ( ( x d y ) = ( z d z ) -> x = y ) ) )
19 14 18 raleqbidva 
 |-  ( ( ( ( p = P /\ d = .- ) /\ x e. P ) /\ y e. P ) -> ( A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) <-> A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) )
20 6 19 raleqbidva 
 |-  ( ( ( p = P /\ d = .- ) /\ x e. P ) -> ( A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) <-> A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) )
21 5 20 raleqbidva 
 |-  ( ( p = P /\ d = .- ) -> ( A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) <-> A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) )
22 13 21 anbi12d 
 |-  ( ( p = P /\ d = .- ) -> ( ( 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 ) ) <-> ( 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 ) ) ) )
23 1 2 22 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 ) ) ) )
24 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 ) ) }
25 23 24 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 ) ) ) )