# 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}\in \mathrm{\infty MetSp}\to {G}\in {𝒢}_{\mathrm{Tarski}}^{C}$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{G}\in \mathrm{\infty MetSp}\to {G}\in \mathrm{V}$
2 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
3 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
4 2 3 xmssym ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge {x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {x}\mathrm{dist}\left({G}\right){y}={y}\mathrm{dist}\left({G}\right){x}$
5 4 3expb ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\right)\to {x}\mathrm{dist}\left({G}\right){y}={y}\mathrm{dist}\left({G}\right){x}$
6 5 ralrimivva ${⊢}{G}\in \mathrm{\infty MetSp}\to \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\mathrm{dist}\left({G}\right){y}={y}\mathrm{dist}\left({G}\right){x}$
7 simpl ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to {G}\in \mathrm{\infty MetSp}$
8 simpr3 ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to {z}\in {\mathrm{Base}}_{{G}}$
9 equid ${⊢}{z}={z}$
10 2 3 xmseq0 ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge {z}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\to \left({z}\mathrm{dist}\left({G}\right){z}=0↔{z}={z}\right)$
11 9 10 mpbiri ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge {z}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\to {z}\mathrm{dist}\left({G}\right){z}=0$
12 7 8 8 11 syl3anc ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to {z}\mathrm{dist}\left({G}\right){z}=0$
13 12 eqeq2d ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}\mathrm{dist}\left({G}\right){y}={z}\mathrm{dist}\left({G}\right){z}↔{x}\mathrm{dist}\left({G}\right){y}=0\right)$
14 2 3 xmseq0 ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge {x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to \left({x}\mathrm{dist}\left({G}\right){y}=0↔{x}={y}\right)$
15 14 3adant3r3 ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}\mathrm{dist}\left({G}\right){y}=0↔{x}={y}\right)$
16 13 15 bitrd ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}\mathrm{dist}\left({G}\right){y}={z}\mathrm{dist}\left({G}\right){z}↔{x}={y}\right)$
17 16 biimpd ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}\mathrm{dist}\left({G}\right){y}={z}\mathrm{dist}\left({G}\right){z}\to {x}={y}\right)$
18 17 ralrimivvva ${⊢}{G}\in \mathrm{\infty MetSp}\to \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{dist}\left({G}\right){y}={z}\mathrm{dist}\left({G}\right){z}\to {x}={y}\right)$
19 6 18 jca ${⊢}{G}\in \mathrm{\infty MetSp}\to \left(\forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\mathrm{dist}\left({G}\right){y}={y}\mathrm{dist}\left({G}\right){x}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{dist}\left({G}\right){y}={z}\mathrm{dist}\left({G}\right){z}\to {x}={y}\right)\right)$
20 eqid ${⊢}\mathrm{Itv}\left({G}\right)=\mathrm{Itv}\left({G}\right)$
21 2 3 20 istrkgc ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}^{C}↔\left({G}\in \mathrm{V}\wedge \left(\forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}{x}\mathrm{dist}\left({G}\right){y}={y}\mathrm{dist}\left({G}\right){x}\wedge \forall {x}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{G}}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{dist}\left({G}\right){y}={z}\mathrm{dist}\left({G}\right){z}\to {x}={y}\right)\right)\right)$
22 1 19 21 sylanbrc ${⊢}{G}\in \mathrm{\infty MetSp}\to {G}\in {𝒢}_{\mathrm{Tarski}}^{C}$