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 \in CMetSp \land W \in CPreHil) \land U \in S) \to X \in CMetSp$

Proof

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

Metamath Proof Explorer

Theorem cmscsscms

Proof