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	|- X = ( W |`s U )
	cssbn.s	|- S = ( LSubSp ` W )
	cssbn.d	|- D = ( ( dist ` W ) |` ( U X. U ) )
Assertion	cssbn	|- ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. Ban )

Proof

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