Theorem reust

Description: The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018)

	Ref	Expression
Assertion	reust	⊢ ( UnifSt ‘ ℝfld ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
2	1	fveq2i	⊢ ( UnifSt ‘ ℝfld ) = ( UnifSt ‘ ( ℂfld ↾s ℝ ) )
3		reex	⊢ ℝ ∈ V
4		ressuss	⊢ ( ℝ ∈ V → ( UnifSt ‘ ( ℂfld ↾s ℝ ) ) = ( ( UnifSt ‘ ℂfld ) ↾t ( ℝ × ℝ ) ) )
5	3 4	ax-mp	⊢ ( UnifSt ‘ ( ℂfld ↾s ℝ ) ) = ( ( UnifSt ‘ ℂfld ) ↾t ( ℝ × ℝ ) )
6		eqid	⊢ ( UnifSt ‘ ℂfld ) = ( UnifSt ‘ ℂfld )
7	6	cnflduss	⊢ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) )
8	7	oveq1i	⊢ ( ( UnifSt ‘ ℂfld ) ↾t ( ℝ × ℝ ) ) = ( ( metUnif ‘ ( abs ∘ − ) ) ↾t ( ℝ × ℝ ) )
9	2 5 8	3eqtri	⊢ ( UnifSt ‘ ℝfld ) = ( ( metUnif ‘ ( abs ∘ − ) ) ↾t ( ℝ × ℝ ) )
10		0re	⊢ 0 ∈ ℝ
11	10	ne0ii	⊢ ℝ ≠ ∅
12		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
13		xmetpsmet	⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ( abs ∘ − ) ∈ ( PsMet ‘ ℂ ) )
14	12 13	ax-mp	⊢ ( abs ∘ − ) ∈ ( PsMet ‘ ℂ )
15		ax-resscn	⊢ ℝ ⊆ ℂ
16		restmetu	⊢ ( ( ℝ ≠ ∅ ∧ ( abs ∘ − ) ∈ ( PsMet ‘ ℂ ) ∧ ℝ ⊆ ℂ ) → ( ( metUnif ‘ ( abs ∘ − ) ) ↾t ( ℝ × ℝ ) ) = ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) )
17	11 14 15 16	mp3an	⊢ ( ( metUnif ‘ ( abs ∘ − ) ) ↾t ( ℝ × ℝ ) ) = ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
18		reds	⊢ ( abs ∘ − ) = ( dist ‘ ℝfld )
19	18	reseq1i	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) )
20	19	fveq2i	⊢ ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) )
21	9 17 20	3eqtri	⊢ ( UnifSt ‘ ℝfld ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) )