Metamath Proof Explorer

Theorem csschl

Description: A complete subspace of a complex pre-Hilbert space is a complex Hilbert space. Remarks: (a) 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. (b) This theorem does not hold for arbitrary subcomplex (pre-)Hilbert spaces, because the scalar field as restriction of the field of the complex numbers need not be closed. (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 ) )
csschl.c 
|- ( Scalar ` W ) = CCfld
Assertion csschl 
|- ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( X e. CHil /\ ( Scalar ` X ) = CCfld ) )

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 csschl.c 
 |-  ( Scalar ` W ) = CCfld
5 cphnvc 
 |-  ( W e. CPreHil -> W e. NrmVec )
6 5 3ad2ant1 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> W e. NrmVec )
7 cncms 
 |-  CCfld e. CMetSp
8 eleq1 
 |-  ( ( Scalar ` W ) = CCfld -> ( ( Scalar ` W ) e. CMetSp <-> CCfld e. CMetSp ) )
9 7 8 mpbiri 
 |-  ( ( Scalar ` W ) = CCfld -> ( Scalar ` W ) e. CMetSp )
10 4 9 mp1i 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( Scalar ` W ) e. CMetSp )
11 simp2 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> U e. S )
12 simp3 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) )
13 1 2 3 cssbn 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. Ban )
14 6 10 11 12 13 syl31anc 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. Ban )
15 1 2 cphssphl 
 |-  ( ( W e. CPreHil /\ U e. S /\ X e. Ban ) -> X e. CHil )
16 14 15 syld3an3 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. CHil )
17 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
18 1 17 resssca 
 |-  ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) )
19 18 4 eqtr3di 
 |-  ( U e. S -> ( Scalar ` X ) = CCfld )
20 19 3ad2ant2 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( Scalar ` X ) = CCfld )
21 16 20 jca 
 |-  ( ( W e. CPreHil /\ U e. S /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( X e. CHil /\ ( Scalar ` X ) = CCfld ) )