Metamath Proof Explorer

Theorem cssbn

Description: A complete subspace of a normed vector space with a complete scalar field is a Banach space. Remark: In contrast to ClSubSp , a complete subspace is defined by "a linear subspace in which all Cauchy sequences converge to a point in the subspace". This is closer to the original, but deprecated definition CH ( df-ch ) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn . (Contributed by NM, 10-Apr-2008) (Revised by AV, 6-Oct-2022)

Ref Expression
Hypotheses cssbn.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
cssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
cssbn.d ⊢ 𝐷 = ( ( dist ‘ 𝑊 ) ↾ ( 𝑈 × 𝑈 ) )
Assertion cssbn ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ Ban )

Proof

Step Hyp Ref Expression
1 cssbn.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 cssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 cssbn.d ⊢ 𝐷 = ( ( dist ‘ 𝑊 ) ↾ ( 𝑈 × 𝑈 ) )
4 simpl1 ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑊 ∈ NrmVec )
5 simpl2 ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
6 nvcnlm ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod )
7 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
8 6 7 syl ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmGrp )
9 nvclmod ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ LMod )
10 2 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
11 9 10 sylan ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
12 1 subgngp ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑋 ∈ NrmGrp )
13 8 11 12 syl2an2r ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmGrp )
14 13 3adant2 ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmGrp )
15 14 adantr ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ NrmGrp )
16 ngpms ⊢ ( 𝑋 ∈ NrmGrp → 𝑋 ∈ MetSp )
17 15 16 syl ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ MetSp )
18 eqid ⊢ ( dist ‘ 𝑊 ) = ( dist ‘ 𝑊 )
19 1 18 ressds ⊢ ( 𝑈 ∈ 𝑆 → ( dist ‘ 𝑊 ) = ( dist ‘ 𝑋 ) )
20 19 3ad2ant3 ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( dist ‘ 𝑊 ) = ( dist ‘ 𝑋 ) )
21 11 3adant2 ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
22 1 subgbas ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
23 21 22 syl ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( Base ‘ 𝑋 ) )
24 23 sqxpeqd ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( 𝑈 × 𝑈 ) = ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) )
25 20 24 reseq12d ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( ( dist ‘ 𝑊 ) ↾ ( 𝑈 × 𝑈 ) ) = ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) )
26 3 25 syl5eq ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝐷 = ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) )
27 26 eqcomd ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) = 𝐷 )
28 27 adantr ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) = 𝐷 )
29 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
30 eqid ⊢ ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) = ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) )
31 29 30 ngpmet ⊢ ( 𝑋 ∈ NrmGrp → ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑋 ) ) )
32 14 31 syl ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑋 ) ) )
33 26 32 eqeltrd ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝐷 ∈ ( Met ‘ ( Base ‘ 𝑋 ) ) )
34 33 adantr ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝐷 ∈ ( Met ‘ ( Base ‘ 𝑋 ) ) )
35 simpr ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
36 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
37 36 iscmet2 ⊢ ( 𝐷 ∈ ( CMet ‘ ( Base ‘ 𝑋 ) ) ↔ ( 𝐷 ∈ ( Met ‘ ( Base ‘ 𝑋 ) ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) )
38 34 35 37 sylanbrc ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝐷 ∈ ( CMet ‘ ( Base ‘ 𝑋 ) ) )
39 28 38 eqeltrd ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝑋 ) ) )
40 29 30 iscms ⊢ ( 𝑋 ∈ CMetSp ↔ ( 𝑋 ∈ MetSp ∧ ( ( dist ‘ 𝑋 ) ↾ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝑋 ) ) ) )
41 17 39 40 sylanbrc ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ CMetSp )
42 simpl3 ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑈 ∈ 𝑆 )
43 1 2 cmslssbn ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → 𝑋 ∈ Ban )
44 4 5 41 42 43 syl22anc ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ Ban )