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 𝑠 U
cssbn.s S = LSubSp W
cssbn.d D = dist W U × U
csschl.c Scalar W = fld
Assertion csschl W CPreHil U S Cau D dom t MetOpen D X ℂHil Scalar X = fld

Proof

Step Hyp Ref Expression
1 cssbn.x X = W 𝑠 U
2 cssbn.s S = LSubSp W
3 cssbn.d D = dist W U × U
4 csschl.c Scalar W = fld
5 cphnvc W CPreHil W NrmVec
6 5 3ad2ant1 W CPreHil U S Cau D dom t MetOpen D W NrmVec
7 cncms fld CMetSp
8 eleq1 Scalar W = fld Scalar W CMetSp fld CMetSp
9 7 8 mpbiri Scalar W = fld Scalar W CMetSp
10 4 9 mp1i W CPreHil U S Cau D dom t MetOpen D Scalar W CMetSp
11 simp2 W CPreHil U S Cau D dom t MetOpen D U S
12 simp3 W CPreHil U S Cau D dom t MetOpen D Cau D dom t MetOpen D
13 1 2 3 cssbn W NrmVec Scalar W CMetSp U S Cau D dom t MetOpen D X Ban
14 6 10 11 12 13 syl31anc W CPreHil U S Cau D dom t MetOpen D X Ban
15 1 2 cphssphl W CPreHil U S X Ban X ℂHil
16 14 15 syld3an3 W CPreHil U S Cau D dom t MetOpen D X ℂHil
17 eqid Scalar W = Scalar W
18 1 17 resssca U S Scalar W = Scalar X
19 18 4 eqtr3di U S Scalar X = fld
20 19 3ad2ant2 W CPreHil U S Cau D dom t MetOpen D Scalar X = fld
21 16 20 jca W CPreHil U S Cau D dom t MetOpen D X ℂHil Scalar X = fld