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 
|- K = ( M |`s A )
cmsss.x 
|- X = ( Base ` M )
cmsss.j 
|- J = ( TopOpen ` M )
Assertion cmsss 
|- ( ( M e. CMetSp /\ A C_ X ) -> ( K e. CMetSp <-> A e. ( Clsd ` J ) ) )

Proof

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