Metamath Proof Explorer

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 ↾ ℝ 2

Proof

Step Hyp Ref Expression
1 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
2 1 fveq2i ⊢ UnifSt ⁡ ℝ fld = UnifSt ⁡ ℂ fld ↾ 𝑠 ℝ
3 reex ⊢ ℝ ∈ V
4 ressuss ⊢ ℝ ∈ V → UnifSt ⁡ ℂ fld ↾ 𝑠 ℝ = UnifSt ⁡ ℂ fld ↾ 𝑡 ℝ 2
5 3 4 ax-mp ⊢ UnifSt ⁡ ℂ fld ↾ 𝑠 ℝ = UnifSt ⁡ ℂ fld ↾ 𝑡 ℝ 2
6 eqid ⊢ UnifSt ⁡ ℂ fld = UnifSt ⁡ ℂ fld
7 6 cnflduss ⊢ UnifSt ⁡ ℂ fld = metUnif ⁡ abs ∘ −
8 7 oveq1i ⊢ UnifSt ⁡ ℂ fld ↾ 𝑡 ℝ 2 = metUnif ⁡ abs ∘ − ↾ 𝑡 ℝ 2
9 2 5 8 3eqtri ⊢ UnifSt ⁡ ℝ fld = metUnif ⁡ abs ∘ − ↾ 𝑡 ℝ 2
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 ∘ − ↾ 𝑡 ℝ 2 = metUnif ⁡ abs ∘ − ↾ ℝ 2
17 11 14 15 16 mp3an ⊢ metUnif ⁡ abs ∘ − ↾ 𝑡 ℝ 2 = metUnif ⁡ abs ∘ − ↾ ℝ 2
18 reds ⊢ abs ∘ − = dist ⁡ ℝ fld
19 18 reseq1i ⊢ abs ∘ − ↾ ℝ 2 = dist ⁡ ℝ fld ↾ ℝ 2
20 19 fveq2i ⊢ metUnif ⁡ abs ∘ − ↾ ℝ 2 = metUnif ⁡ dist ⁡ ℝ fld ↾ ℝ 2
21 9 17 20 3eqtri ⊢ UnifSt ⁡ ℝ fld = metUnif ⁡ dist ⁡ ℝ fld ↾ ℝ 2