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∈∞MetSp→G∈𝒢TarskiC

Proof

Step Hyp Ref Expression
1 elex ⊢G∈∞MetSp→G∈V
2 eqid ⊢BaseG=BaseG
3 eqid ⊢dist⁡G=dist⁡G
4 2 3 xmssym ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG→xdist⁡Gy=ydist⁡Gx
5 4 3expb ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG→xdist⁡Gy=ydist⁡Gx
6 5 ralrimivva ⊢G∈∞MetSp→∀x∈BaseG∀y∈BaseGxdist⁡Gy=ydist⁡Gx
7 simpl ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG∧z∈BaseG→G∈∞MetSp
8 simpr3 ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG∧z∈BaseG→z∈BaseG
9 equid ⊢z=z
10 2 3 xmseq0 ⊢G∈∞MetSp∧z∈BaseG∧z∈BaseG→zdist⁡Gz=0↔z=z
11 9 10 mpbiri ⊢G∈∞MetSp∧z∈BaseG∧z∈BaseG→zdist⁡Gz=0
12 7 8 8 11 syl3anc ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG∧z∈BaseG→zdist⁡Gz=0
13 12 eqeq2d ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG∧z∈BaseG→xdist⁡Gy=zdist⁡Gz↔xdist⁡Gy=0
14 2 3 xmseq0 ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG→xdist⁡Gy=0↔x=y
15 14 3adant3r3 ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG∧z∈BaseG→xdist⁡Gy=0↔x=y
16 13 15 bitrd ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG∧z∈BaseG→xdist⁡Gy=zdist⁡Gz↔x=y
17 16 biimpd ⊢G∈∞MetSp∧x∈BaseG∧y∈BaseG∧z∈BaseG→xdist⁡Gy=zdist⁡Gz→x=y
18 17 ralrimivvva ⊢G∈∞MetSp→∀x∈BaseG∀y∈BaseG∀z∈BaseGxdist⁡Gy=zdist⁡Gz→x=y
19 6 18 jca ⊢G∈∞MetSp→∀x∈BaseG∀y∈BaseGxdist⁡Gy=ydist⁡Gx∧∀x∈BaseG∀y∈BaseG∀z∈BaseGxdist⁡Gy=zdist⁡Gz→x=y
20 eqid ⊢Itv⁡G=Itv⁡G
21 2 3 20 istrkgc ⊢G∈𝒢TarskiC↔G∈V∧∀x∈BaseG∀y∈BaseGxdist⁡Gy=ydist⁡Gx∧∀x∈BaseG∀y∈BaseG∀z∈BaseGxdist⁡Gy=zdist⁡Gz→x=y
22 1 19 21 sylanbrc ⊢G∈∞MetSp→G∈𝒢TarskiC