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	$⊢ X = W ↾_{𝑠} U$
	cssbn.s	$⊢ S = LSubSp (W)$
	cssbn.d	$⊢ D = {dist (W) ↾}_{(U \times U)}$
Assertion	cssbn	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to X \in Ban$

Proof

Step	Hyp	Ref	Expression
1		cssbn.x	$⊢ X = W ↾_{𝑠} U$
2		cssbn.s	$⊢ S = LSubSp (W)$
3		cssbn.d	$⊢ D = {dist (W) ↾}_{(U \times U)}$
4		simpl1	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to W \in NrmVec$
5		simpl2	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to Scalar (W) \in CMetSp$
6		nvcnlm	$⊢ W \in NrmVec \to W \in NrmMod$
7		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
8	6 7	syl	$⊢ W \in NrmVec \to W \in NrmGrp$
9		nvclmod	$⊢ W \in NrmVec \to W \in LMod$
10	2	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$
11	9 10	sylan	$⊢ (W \in NrmVec \land U \in S) \to U \in SubGrp (W)$
12	1	subgngp	$⊢ (W \in NrmGrp \land U \in SubGrp (W)) \to X \in NrmGrp$
13	8 11 12	syl2an2r	$⊢ (W \in NrmVec \land U \in S) \to X \in NrmGrp$
14	13	3adant2	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to X \in NrmGrp$
15	14	adantr	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to X \in NrmGrp$
16		ngpms	$⊢ X \in NrmGrp \to X \in MetSp$
17	15 16	syl	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to X \in MetSp$
18		eqid	$⊢ dist (W) = dist (W)$
19	1 18	ressds	$⊢ U \in S \to dist (W) = dist (X)$
20	19	3ad2ant3	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to dist (W) = dist (X)$
21	11	3adant2	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to U \in SubGrp (W)$
22	1	subgbas	$⊢ U \in SubGrp (W) \to U = {Base}_{X}$
23	21 22	syl	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to U = {Base}_{X}$
24	23	sqxpeqd	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to U \times U = {Base}_{X} \times {Base}_{X}$
25	20 24	reseq12d	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to {dist (W) ↾}_{(U \times U)} = {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})}$
26	3 25	syl5eq	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to D = {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})}$
27	26	eqcomd	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})} = D$
28	27	adantr	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})} = D$
29		eqid	$⊢ {Base}_{X} = {Base}_{X}$
30		eqid	$⊢ {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})} = {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})}$
31	29 30	ngpmet	$⊢ X \in NrmGrp \to {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})} \in Met ({Base}_{X})$
32	14 31	syl	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})} \in Met ({Base}_{X})$
33	26 32	eqeltrd	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \to D \in Met ({Base}_{X})$
34	33	adantr	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to D \in Met ({Base}_{X})$
35		simpr	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))$
36		eqid	$⊢ MetOpen (D) = MetOpen (D)$
37	36	iscmet2	$⊢ D \in CMet ({Base}_{X}) \leftrightarrow (D \in Met ({Base}_{X}) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D)))$
38	34 35 37	sylanbrc	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to D \in CMet ({Base}_{X})$
39	28 38	eqeltrd	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})} \in CMet ({Base}_{X})$
40	29 30	iscms	$⊢ X \in CMetSp \leftrightarrow (X \in MetSp \land {dist (X) ↾}_{({Base}_{X} \times {Base}_{X})} \in CMet ({Base}_{X}))$
41	17 39 40	sylanbrc	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to X \in CMetSp$
42		simpl3	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to U \in S$
43	1 2	cmslssbn	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp) \land (X \in CMetSp \land U \in S)) \to X \in Ban$
44	4 5 41 42 43	syl22anc	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp \land U \in S) \land Cau (D) \subseteq dom \underset{t}{⇝} (MetOpen (D))) \to X \in Ban$

Metamath Proof Explorer

Theorem cssbn

Proof