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 ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )