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