Metamath Proof Explorer

Theorem 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 ⊢ 𝐾 = ( 𝑀 ↾s 𝐴 )
cmsss.x ⊢ 𝑋 = ( Base ‘ 𝑀 )
cmsss.j ⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
Assertion cmsss ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐾 ∈ CMetSp ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 cmsss.h ⊢ 𝐾 = ( 𝑀 ↾s 𝐴 )
2 cmsss.x ⊢ 𝑋 = ( Base ‘ 𝑀 )
3 cmsss.j ⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
4 simpr ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
5 xpss12 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 × 𝐴 ) ⊆ ( 𝑋 × 𝑋 ) )
6 4 5 sylancom ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 × 𝐴 ) ⊆ ( 𝑋 × 𝑋 ) )
7 6 resabs1d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝐴 × 𝐴 ) ) )
8 2 fvexi ⊢ 𝑋 ∈ V
9 8 ssex ⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 ∈ V )
10 9 adantl ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
11 eqid ⊢ ( dist ‘ 𝑀 ) = ( dist ‘ 𝑀 )
12 1 11 ressds ⊢ ( 𝐴 ∈ V → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) )
13 10 12 syl ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) )
14 1 2 ressbas2 ⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 = ( Base ‘ 𝐾 ) )
15 14 adantl ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ( Base ‘ 𝐾 ) )
16 15 sqxpeqd ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 × 𝐴 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
17 13 16 reseq12d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( dist ‘ 𝑀 ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
18 7 17 eqtrd ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
19 15 fveq2d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( CMet ‘ 𝐴 ) = ( CMet ‘ ( Base ‘ 𝐾 ) ) )
20 18 19 eleq12d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ↔ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) )
21 eqid ⊢ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
22 2 21 cmscmet ⊢ ( 𝑀 ∈ CMetSp → ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( CMet ‘ 𝑋 ) )
23 22 adantr ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( CMet ‘ 𝑋 ) )
24 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
25 24 cmetss ⊢ ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( CMet ‘ 𝑋 ) → ( ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ↔ 𝐴 ∈ ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) ) )
26 23 25 syl ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ↔ 𝐴 ∈ ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) ) )
27 20 26 bitr3d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ↔ 𝐴 ∈ ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) ) )
28 cmsms ⊢ ( 𝑀 ∈ CMetSp → 𝑀 ∈ MetSp )
29 ressms ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ∈ V ) → ( 𝑀 ↾s 𝐴 ) ∈ MetSp )
30 1 29 eqeltrid ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ∈ V ) → 𝐾 ∈ MetSp )
31 28 9 30 syl2an ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → 𝐾 ∈ MetSp )
32 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33 eqid ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
34 32 33 iscms ⊢ ( 𝐾 ∈ CMetSp ↔ ( 𝐾 ∈ MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) )
35 34 baib ⊢ ( 𝐾 ∈ MetSp → ( 𝐾 ∈ CMetSp ↔ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) )
36 31 35 syl ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐾 ∈ CMetSp ↔ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) )
37 28 adantr ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → 𝑀 ∈ MetSp )
38 3 2 21 mstopn ⊢ ( 𝑀 ∈ MetSp → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) )
39 37 38 syl ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) )
40 39 fveq2d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( Clsd ‘ 𝐽 ) = ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) )
41 40 eleq2d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) ) )
42 27 36 41 3bitr4d ⊢ ( ( 𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐾 ∈ CMetSp ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )