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 ( 𝐺 ∈ ∞MetSp → 𝐺 ∈ TarskiGC )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐺 ∈ ∞MetSp → 𝐺 ∈ V )
2 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
4 2 3 xmssym ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
5 4 3expb ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
6 5 ralrimivva ⊢ ( 𝐺 ∈ ∞MetSp → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
7 simpl ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝐺 ∈ ∞MetSp )
8 simpr3 ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
9 equid ⊢ 𝑧 = 𝑧
10 2 3 xmseq0 ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) = 0 ↔ 𝑧 = 𝑧 ) )
11 9 10 mpbiri ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) = 0 )
12 7 8 8 11 syl3anc ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) = 0 )
13 12 eqeq2d ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) ↔ ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = 0 ) )
14 2 3 xmseq0 ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
15 14 3adant3r3 ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
16 13 15 bitrd ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) ↔ 𝑥 = 𝑦 ) )
17 16 biimpd ⊢ ( ( 𝐺 ∈ ∞MetSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) → 𝑥 = 𝑦 ) )
18 17 ralrimivvva ⊢ ( 𝐺 ∈ ∞MetSp → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) → 𝑥 = 𝑦 ) )
19 6 18 jca ⊢ ( 𝐺 ∈ ∞MetSp → ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) → 𝑥 = 𝑦 ) ) )
20 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
21 2 3 20 istrkgc ⊢ ( 𝐺 ∈ TarskiGC ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( dist ‘ 𝐺 ) 𝑧 ) → 𝑥 = 𝑦 ) ) ) )
22 1 19 21 sylanbrc ⊢ ( 𝐺 ∈ ∞MetSp → 𝐺 ∈ TarskiGC )