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 𝑠 U
cmscsscms.s S = ClSubSp W
Assertion cmscsscms W CMetSp W CPreHil U S X CMetSp

Proof

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