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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
cmscsscms.s ⊢ 𝑆 = ( ClSubSp ‘ 𝑊 )
Assertion cmscsscms ( ( ( 𝑊 ∈ CMetSp ∧ 𝑊 ∈ ℂPreHil ) ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ CMetSp )

Proof

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