cmsss

Description: The restriction of a complete metric space is complete iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	cmsss.h	$⊢ K = M ↾_{𝑠} A$
	cmsss.x	$⊢ X = {Base}_{M}$
	cmsss.j	$⊢ J = TopOpen (M)$
Assertion	cmsss	$⊢ (M \in CMetSp \land A \subseteq X) \to (K \in CMetSp \leftrightarrow A \in Clsd (J))$

Proof

Step	Hyp	Ref	Expression
1		cmsss.h	$⊢ K = M ↾_{𝑠} A$
2		cmsss.x	$⊢ X = {Base}_{M}$
3		cmsss.j	$⊢ J = TopOpen (M)$
4		simpr	$⊢ (M \in CMetSp \land A \subseteq X) \to A \subseteq X$
5		xpss12	$⊢ (A \subseteq X \land A \subseteq X) \to A \times A \subseteq X \times X$
6	4 5	sylancom	$⊢ (M \in CMetSp \land A \subseteq X) \to A \times A \subseteq X \times X$
7	6	resabs1d	$⊢ (M \in CMetSp \land A \subseteq X) \to {({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} = {dist (M) ↾}_{(A \times A)}$
8	2	fvexi	$⊢ X \in V$
9	8	ssex	$⊢ A \subseteq X \to A \in V$
10	9	adantl	$⊢ (M \in CMetSp \land A \subseteq X) \to A \in V$
11		eqid	$⊢ dist (M) = dist (M)$
12	1 11	ressds	$⊢ A \in V \to dist (M) = dist (K)$
13	10 12	syl	$⊢ (M \in CMetSp \land A \subseteq X) \to dist (M) = dist (K)$
14	1 2	ressbas2	$⊢ A \subseteq X \to A = {Base}_{K}$
15	14	adantl	$⊢ (M \in CMetSp \land A \subseteq X) \to A = {Base}_{K}$
16	15	sqxpeqd	$⊢ (M \in CMetSp \land A \subseteq X) \to A \times A = {Base}_{K} \times {Base}_{K}$
17	13 16	reseq12d	$⊢ (M \in CMetSp \land A \subseteq X) \to {dist (M) ↾}_{(A \times A)} = {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}$
18	7 17	eqtrd	$⊢ (M \in CMetSp \land A \subseteq X) \to {({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} = {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}$
19	15	fveq2d	$⊢ (M \in CMetSp \land A \subseteq X) \to CMet (A) = CMet ({Base}_{K})$
20	18 19	eleq12d	$⊢ (M \in CMetSp \land A \subseteq X) \to ({({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} \in CMet (A) \leftrightarrow {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}))$
21		eqid	$⊢ {dist (M) ↾}_{(X \times X)} = {dist (M) ↾}_{(X \times X)}$
22	2 21	cmscmet	$⊢ M \in CMetSp \to {dist (M) ↾}_{(X \times X)} \in CMet (X)$
23	22	adantr	$⊢ (M \in CMetSp \land A \subseteq X) \to {dist (M) ↾}_{(X \times X)} \in CMet (X)$
24		eqid	$⊢ MetOpen ({dist (M) ↾}_{(X \times X)}) = MetOpen ({dist (M) ↾}_{(X \times X)})$
25	24	cmetss	$⊢ {dist (M) ↾}_{(X \times X)} \in CMet (X) \to ({({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} \in CMet (A) \leftrightarrow A \in Clsd (MetOpen ({dist (M) ↾}_{(X \times X)})))$
26	23 25	syl	$⊢ (M \in CMetSp \land A \subseteq X) \to ({({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} \in CMet (A) \leftrightarrow A \in Clsd (MetOpen ({dist (M) ↾}_{(X \times X)})))$
27	20 26	bitr3d	$⊢ (M \in CMetSp \land A \subseteq X) \to ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}) \leftrightarrow A \in Clsd (MetOpen ({dist (M) ↾}_{(X \times X)})))$
28		cmsms	$⊢ M \in CMetSp \to M \in MetSp$
29		ressms	$⊢ (M \in MetSp \land A \in V) \to M ↾_{𝑠} A \in MetSp$
30	1 29	eqeltrid	$⊢ (M \in MetSp \land A \in V) \to K \in MetSp$
31	28 9 30	syl2an	$⊢ (M \in CMetSp \land A \subseteq X) \to K \in MetSp$
32		eqid	$⊢ {Base}_{K} = {Base}_{K}$
33		eqid	$⊢ {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} = {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}$
34	32 33	iscms	$⊢ K \in CMetSp \leftrightarrow (K \in MetSp \land {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}))$
35	34	baib	$⊢ K \in MetSp \to (K \in CMetSp \leftrightarrow {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}))$
36	31 35	syl	$⊢ (M \in CMetSp \land A \subseteq X) \to (K \in CMetSp \leftrightarrow {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}))$
37	28	adantr	$⊢ (M \in CMetSp \land A \subseteq X) \to M \in MetSp$
38	3 2 21	mstopn	$⊢ M \in MetSp \to J = MetOpen ({dist (M) ↾}_{(X \times X)})$
39	37 38	syl	$⊢ (M \in CMetSp \land A \subseteq X) \to J = MetOpen ({dist (M) ↾}_{(X \times X)})$
40	39	fveq2d	$⊢ (M \in CMetSp \land A \subseteq X) \to Clsd (J) = Clsd (MetOpen ({dist (M) ↾}_{(X \times X)}))$
41	40	eleq2d	$⊢ (M \in CMetSp \land A \subseteq X) \to (A \in Clsd (J) \leftrightarrow A \in Clsd (MetOpen ({dist (M) ↾}_{(X \times X)})))$
42	27 36 41	3bitr4d	$⊢ (M \in CMetSp \land A \subseteq X) \to (K \in CMetSp \leftrightarrow A \in Clsd (J))$

Metamath Proof Explorer

Theorem cmsss

Proof