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