This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ismet2

Description: An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion ismet2 ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝑋 ∈ V )
2 elfvex ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ V )
3 2 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) → 𝑋 ∈ V )
4 simpllr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
5 simpr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
6 simplrl ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
7 4 5 6 fovcdmd ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑥 ) ∈ ℝ )
8 simplrr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
9 4 5 8 fovcdmd ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ )
10 7 9 rexaddd ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
11 10 breq2d ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) )
12 11 ralbidva ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) )
13 12 anbi2d ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) )
14 13 2ralbidva ⊢ ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) )
15 simpr ⊢ ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
16 ressxr ⊢ ℝ ⊆ ℝ*
17 fss ⊢ ( ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
18 15 16 17 sylancl ⊢ ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
19 18 biantrurd ⊢ ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
20 14 19 bitr3d ⊢ ( ( 𝑋 ∈ V ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
21 20 pm5.32da ⊢ ( 𝑋 ∈ V → ( ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) ) )
22 21 biancomd ⊢ ( 𝑋 ∈ V → ( ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) ↔ ( ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ) )
23 ismet ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
24 isxmet ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
25 24 anbi1d ⊢ ( 𝑋 ∈ V → ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ↔ ( ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ) )
26 22 23 25 3bitr4d ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) ) )
27 1 3 26 pm5.21nii ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )