xmsusp

Description: If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017)

	Ref	Expression
Hypotheses	xmsusp.x	$⊢ X = {Base}_{F}$
	xmsusp.d	$⊢ D = {dist (F) ↾}_{(X \times X)}$
	xmsusp.u	$⊢ U = UnifSt (F)$
Assertion	xmsusp	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to F \in UnifSp$

Proof

Step	Hyp	Ref	Expression
1		xmsusp.x	$⊢ X = {Base}_{F}$
2		xmsusp.d	$⊢ D = {dist (F) ↾}_{(X \times X)}$
3		xmsusp.u	$⊢ U = UnifSt (F)$
4		simp3	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to U = metUnif (D)$
5		simp1	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to X \neq \emptyset$
6	1 2	xmsxmet	$⊢ F \in ∞MetSp \to D \in ∞Met (X)$
7	6	3ad2ant2	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to D \in ∞Met (X)$
8		xmetpsmet	$⊢ D \in ∞Met (X) \to D \in PsMet (X)$
9		metuust	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to metUnif (D) \in UnifOn (X)$
10	8 9	sylan2	$⊢ (X \neq \emptyset \land D \in ∞Met (X)) \to metUnif (D) \in UnifOn (X)$
11	5 7 10	syl2anc	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to metUnif (D) \in UnifOn (X)$
12	4 11	eqeltrd	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to U \in UnifOn (X)$
13		xmetutop	$⊢ (X \neq \emptyset \land D \in ∞Met (X)) \to unifTop (metUnif (D)) = MetOpen (D)$
14	5 7 13	syl2anc	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to unifTop (metUnif (D)) = MetOpen (D)$
15	4	fveq2d	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to unifTop (U) = unifTop (metUnif (D))$
16		eqid	$⊢ TopOpen (F) = TopOpen (F)$
17	16 1 2	xmstopn	$⊢ F \in ∞MetSp \to TopOpen (F) = MetOpen (D)$
18	17	3ad2ant2	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to TopOpen (F) = MetOpen (D)$
19	14 15 18	3eqtr4rd	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to TopOpen (F) = unifTop (U)$
20	1 3 16	isusp	$⊢ F \in UnifSp \leftrightarrow (U \in UnifOn (X) \land TopOpen (F) = unifTop (U))$
21	12 19 20	sylanbrc	$⊢ (X \neq \emptyset \land F \in ∞MetSp \land U = metUnif (D)) \to F \in UnifSp$

Metamath Proof Explorer

Theorem xmsusp

Proof