This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
cssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
cssbn.d ⊢ 𝐷 = ( ( dist ‘ 𝑊 ) ↾ ( 𝑈 × 𝑈 ) )
csschl.c ⊢ ( Scalar ‘ 𝑊 ) = ℂfld
Assertion csschl ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( 𝑋 ∈ ℂHil ∧ ( Scalar ‘ 𝑋 ) = ℂfld ) )

Proof

Step Hyp Ref Expression
1 cssbn.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 cssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 cssbn.d ⊢ 𝐷 = ( ( dist ‘ 𝑊 ) ↾ ( 𝑈 × 𝑈 ) )
4 csschl.c ⊢ ( Scalar ‘ 𝑊 ) = ℂfld
5 cphnvc ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmVec )
6 5 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑊 ∈ NrmVec )
7 cncms ⊢ ℂfld ∈ CMetSp
8 eleq1 ⊢ ( ( Scalar ‘ 𝑊 ) = ℂfld → ( ( Scalar ‘ 𝑊 ) ∈ CMetSp ↔ ℂfld ∈ CMetSp ) )
9 7 8 mpbiri ⊢ ( ( Scalar ‘ 𝑊 ) = ℂfld → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
10 4 9 mp1i ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
11 simp2 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑈 ∈ 𝑆 )
12 simp3 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
13 1 2 3 cssbn ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ Ban )
14 6 10 11 12 13 syl31anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ Ban )
15 1 2 cphssphl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ Ban ) → 𝑋 ∈ ℂHil )
16 14 15 syld3an3 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → 𝑋 ∈ ℂHil )
17 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
18 1 17 resssca ⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
19 18 4 eqtr3di ⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑋 ) = ℂfld )
20 19 3ad2ant2 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( Scalar ‘ 𝑋 ) = ℂfld )
21 16 20 jca ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( 𝑋 ∈ ℂHil ∧ ( Scalar ‘ 𝑋 ) = ℂfld ) )