Metamath Proof Explorer

Theorem xrsdsre

Description: The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis xrsxmet.1 ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
Assertion xrsdsre ( 𝐷 ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )

Proof

Step Hyp Ref Expression
1 xrsxmet.1 ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
2 1 xrsdsreval ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 𝐷 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
3 ovres ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ( 𝐷 ↾ ( ℝ × ℝ ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
4 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
5 4 remetdval ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
6 2 3 5 3eqtr4d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ( 𝐷 ↾ ( ℝ × ℝ ) ) 𝑦 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑦 ) )
7 6 rgen2 ⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 ( 𝐷 ↾ ( ℝ × ℝ ) ) 𝑦 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑦 )
8 1 xrsxmet ⊢ 𝐷 ∈ ( ∞Met ‘ ℝ* )
9 xmetf ⊢ ( 𝐷 ∈ ( ∞Met ‘ ℝ* ) → 𝐷 : ( ℝ* × ℝ* ) ⟶ ℝ* )
10 ffn ⊢ ( 𝐷 : ( ℝ* × ℝ* ) ⟶ ℝ* → 𝐷 Fn ( ℝ* × ℝ* ) )
11 8 9 10 mp2b ⊢ 𝐷 Fn ( ℝ* × ℝ* )
12 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
13 fnssres ⊢ ( ( 𝐷 Fn ( ℝ* × ℝ* ) ∧ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) ) → ( 𝐷 ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) )
14 11 12 13 mp2an ⊢ ( 𝐷 ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ )
15 cnmet ⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )
16 metf ⊢ ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
17 ffn ⊢ ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ → ( abs ∘ − ) Fn ( ℂ × ℂ ) )
18 15 16 17 mp2b ⊢ ( abs ∘ − ) Fn ( ℂ × ℂ )
19 ax-resscn ⊢ ℝ ⊆ ℂ
20 xpss12 ⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
21 19 19 20 mp2an ⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
22 fnssres ⊢ ( ( ( abs ∘ − ) Fn ( ℂ × ℂ ) ∧ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) ) → ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) )
23 18 21 22 mp2an ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ )
24 eqfnov2 ⊢ ( ( ( 𝐷 ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) ∧ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) ) → ( ( 𝐷 ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 ( 𝐷 ↾ ( ℝ × ℝ ) ) 𝑦 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑦 ) ) )
25 14 23 24 mp2an ⊢ ( ( 𝐷 ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 ( 𝐷 ↾ ( ℝ × ℝ ) ) 𝑦 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑦 ) )
26 7 25 mpbir ⊢ ( 𝐷 ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )