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 ) )