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 ∈ 𝒢 Tarski C

Proof

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