Metamath Proof Explorer

Theorem cmscsscms

Description: A closed subspace of a complete metric space which is also a subcomplex pre-Hilbert space is a complete metric space. Remark: the assumption that the Banach space must be a (subcomplex) pre-Hilbert space is required because the definition of ClSubSp is based on an inner product. If ClSubSp was generalized to arbitrary topological spaces (or at least topological modules), this assumption could be omitted. (Contributed by AV, 8-Oct-2022)

Ref Expression
Hypotheses cmslssbn.x 
|- X = ( W |`s U )
cmscsscms.s 
|- S = ( ClSubSp ` W )
Assertion cmscsscms 
|- ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> X e. CMetSp )

Proof

Step Hyp Ref Expression
1 cmslssbn.x 
 |-  X = ( W |`s U )
2 cmscsscms.s 
 |-  S = ( ClSubSp ` W )
3 cmsms 
 |-  ( W e. CMetSp -> W e. MetSp )
4 3 adantr 
 |-  ( ( W e. CMetSp /\ W e. CPreHil ) -> W e. MetSp )
5 ressms 
 |-  ( ( W e. MetSp /\ U e. S ) -> ( W |`s U ) e. MetSp )
6 4 5 sylan 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( W |`s U ) e. MetSp )
7 1 6 eqeltrid 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> X e. MetSp )
8 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
9 8 adantl 
 |-  ( ( W e. CMetSp /\ W e. CPreHil ) -> W e. LMod )
10 9 adantr 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> W e. LMod )
11 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
12 11 adantl 
 |-  ( ( W e. CMetSp /\ W e. CPreHil ) -> W e. PreHil )
13 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
14 2 13 csslss 
 |-  ( ( W e. PreHil /\ U e. S ) -> U e. ( LSubSp ` W ) )
15 12 14 sylan 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> U e. ( LSubSp ` W ) )
16 13 lsssubg 
 |-  ( ( W e. LMod /\ U e. ( LSubSp ` W ) ) -> U e. ( SubGrp ` W ) )
17 10 15 16 syl2anc 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> U e. ( SubGrp ` W ) )
18 1 subgbas 
 |-  ( U e. ( SubGrp ` W ) -> U = ( Base ` X ) )
19 17 18 syl 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> U = ( Base ` X ) )
20 eqid 
 |-  ( TopOpen ` W ) = ( TopOpen ` W )
21 2 20 csscld 
 |-  ( ( W e. CPreHil /\ U e. S ) -> U e. ( Clsd ` ( TopOpen ` W ) ) )
22 21 adantll 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> U e. ( Clsd ` ( TopOpen ` W ) ) )
23 19 22 eqeltrrd 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( Base ` X ) e. ( Clsd ` ( TopOpen ` W ) ) )
24 eqid 
 |-  ( dist ` W ) = ( dist ` W )
25 1 24 ressds 
 |-  ( U e. S -> ( dist ` W ) = ( dist ` X ) )
26 25 adantl 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( dist ` W ) = ( dist ` X ) )
27 26 eqcomd 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( dist ` X ) = ( dist ` W ) )
28 27 reseq1d 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) = ( ( dist ` W ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) )
29 19 17 eqeltrrd 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( Base ` X ) e. ( SubGrp ` W ) )
30 eqid 
 |-  ( Base ` W ) = ( Base ` W )
31 30 subgss 
 |-  ( ( Base ` X ) e. ( SubGrp ` W ) -> ( Base ` X ) C_ ( Base ` W ) )
32 29 31 syl 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( Base ` X ) C_ ( Base ` W ) )
33 xpss12 
 |-  ( ( ( Base ` X ) C_ ( Base ` W ) /\ ( Base ` X ) C_ ( Base ` W ) ) -> ( ( Base ` X ) X. ( Base ` X ) ) C_ ( ( Base ` W ) X. ( Base ` W ) ) )
34 32 32 33 syl2anc 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( Base ` X ) X. ( Base ` X ) ) C_ ( ( Base ` W ) X. ( Base ` W ) ) )
35 34 resabs1d 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) = ( ( dist ` W ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) )
36 28 35 eqtr4d 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) = ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) )
37 36 eleq1d 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) <-> ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) ) )
38 eqid 
 |-  ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) = ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) )
39 30 38 cmscmet 
 |-  ( W e. CMetSp -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( CMet ` ( Base ` W ) ) )
40 39 adantr 
 |-  ( ( W e. CMetSp /\ W e. CPreHil ) -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( CMet ` ( Base ` W ) ) )
41 40 adantr 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( CMet ` ( Base ` W ) ) )
42 eqid 
 |-  ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) )
43 42 cmetss 
 |-  ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( CMet ` ( Base ` W ) ) -> ( ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) <-> ( Base ` X ) e. ( Clsd ` ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) ) )
44 41 43 syl 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) <-> ( Base ` X ) e. ( Clsd ` ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) ) )
45 4 adantr 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> W e. MetSp )
46 20 30 38 mstopn 
 |-  ( W e. MetSp -> ( TopOpen ` W ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
47 45 46 syl 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( TopOpen ` W ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
48 47 eqcomd 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) = ( TopOpen ` W ) )
49 48 fveq2d 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( Clsd ` ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) = ( Clsd ` ( TopOpen ` W ) ) )
50 49 eleq2d 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( Base ` X ) e. ( Clsd ` ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) <-> ( Base ` X ) e. ( Clsd ` ( TopOpen ` W ) ) ) )
51 37 44 50 3bitrd 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) <-> ( Base ` X ) e. ( Clsd ` ( TopOpen ` W ) ) ) )
52 23 51 mpbird 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) )
53 eqid 
 |-  ( Base ` X ) = ( Base ` X )
54 eqid 
 |-  ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) = ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) )
55 53 54 iscms 
 |-  ( X e. CMetSp <-> ( X e. MetSp /\ ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) ) )
56 7 52 55 sylanbrc 
 |-  ( ( ( W e. CMetSp /\ W e. CPreHil ) /\ U e. S ) -> X e. CMetSp )