Metamath Proof Explorer

Theorem xmstrkgc

Description: Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019)

Ref Expression
Assertion xmstrkgc 
|- ( G e. *MetSp -> G e. TarskiGC )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( G e. *MetSp -> G e. _V )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 eqid 
 |-  ( dist ` G ) = ( dist ` G )
4 2 3 xmssym 
 |-  ( ( G e. *MetSp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( dist ` G ) y ) = ( y ( dist ` G ) x ) )
5 4 3expb 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( dist ` G ) y ) = ( y ( dist ` G ) x ) )
6 5 ralrimivva 
 |-  ( G e. *MetSp -> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( dist ` G ) y ) = ( y ( dist ` G ) x ) )
7 simpl 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> G e. *MetSp )
8 simpr3 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> z e. ( Base ` G ) )
9 equid 
 |-  z = z
10 2 3 xmseq0 
 |-  ( ( G e. *MetSp /\ z e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( ( z ( dist ` G ) z ) = 0 <-> z = z ) )
11 9 10 mpbiri 
 |-  ( ( G e. *MetSp /\ z e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( z ( dist ` G ) z ) = 0 )
12 7 8 8 11 syl3anc 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( z ( dist ` G ) z ) = 0 )
13 12 eqeq2d 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( dist ` G ) y ) = ( z ( dist ` G ) z ) <-> ( x ( dist ` G ) y ) = 0 ) )
14 2 3 xmseq0 
 |-  ( ( G e. *MetSp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( ( x ( dist ` G ) y ) = 0 <-> x = y ) )
15 14 3adant3r3 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( dist ` G ) y ) = 0 <-> x = y ) )
16 13 15 bitrd 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( dist ` G ) y ) = ( z ( dist ` G ) z ) <-> x = y ) )
17 16 biimpd 
 |-  ( ( G e. *MetSp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( dist ` G ) y ) = ( z ( dist ` G ) z ) -> x = y ) )
18 17 ralrimivvva 
 |-  ( G e. *MetSp -> A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( x ( dist ` G ) y ) = ( z ( dist ` G ) z ) -> x = y ) )
19 6 18 jca 
 |-  ( G e. *MetSp -> ( A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( dist ` G ) y ) = ( y ( dist ` G ) x ) /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( x ( dist ` G ) y ) = ( z ( dist ` G ) z ) -> x = y ) ) )
20 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
21 2 3 20 istrkgc 
 |-  ( G e. TarskiGC <-> ( G e. _V /\ ( A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( dist ` G ) y ) = ( y ( dist ` G ) x ) /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( x ( dist ` G ) y ) = ( z ( dist ` G ) z ) -> x = y ) ) ) )
22 1 19 21 sylanbrc 
 |-  ( G e. *MetSp -> G e. TarskiGC )