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 )