setsms

Description: The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	setsms.x	$⊢ φ \to X = {Base}_{M}$
	setsms.d	$⊢ φ \to D = {dist (M) ↾}_{(X \times X)}$
	setsms.k	$⊢ φ \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
	setsms.m	$⊢ φ \to M \in V$
Assertion	setsms	$⊢ φ \to (K \in MetSp \leftrightarrow D \in Met (X))$

Proof

Step	Hyp	Ref	Expression
1		setsms.x	$⊢ φ \to X = {Base}_{M}$
2		setsms.d	$⊢ φ \to D = {dist (M) ↾}_{(X \times X)}$
3		setsms.k	$⊢ φ \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
4		setsms.m	$⊢ φ \to M \in V$
5	1 2 3 4	setsxms	$⊢ φ \to (K \in ∞MetSp \leftrightarrow D \in ∞Met (X))$
6	1 2 3	setsmsds	$⊢ φ \to dist (M) = dist (K)$
7	1 2 3	setsmsbas	$⊢ φ \to X = {Base}_{K}$
8	7	sqxpeqd	$⊢ φ \to X \times X = {Base}_{K} \times {Base}_{K}$
9	6 8	reseq12d	$⊢ φ \to {dist (M) ↾}_{(X \times X)} = {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}$
10	2 9	eqtr2d	$⊢ φ \to {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} = D$
11	7	fveq2d	$⊢ φ \to Met (X) = Met ({Base}_{K})$
12	11	eqcomd	$⊢ φ \to Met ({Base}_{K}) = Met (X)$
13	10 12	eleq12d	$⊢ φ \to ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in Met ({Base}_{K}) \leftrightarrow D \in Met (X))$
14	5 13	anbi12d	$⊢ φ \to ((K \in ∞MetSp \land {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in Met ({Base}_{K})) \leftrightarrow (D \in ∞Met (X) \land D \in Met (X)))$
15		eqid	$⊢ TopOpen (K) = TopOpen (K)$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17		eqid	$⊢ {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} = {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}$
18	15 16 17	isms	$⊢ K \in MetSp \leftrightarrow (K \in ∞MetSp \land {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in Met ({Base}_{K}))$
19		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
20	19	pm4.71ri	$⊢ D \in Met (X) \leftrightarrow (D \in ∞Met (X) \land D \in Met (X))$
21	14 18 20	3bitr4g	$⊢ φ \to (K \in MetSp \leftrightarrow D \in Met (X))$

Metamath Proof Explorer

Theorem setsms

Proof