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	4 18	syl5reqr	⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑋 ) = ℂfld )
20	19	3ad2ant2	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( Scalar ‘ 𝑋 ) = ℂfld )
21	16 20	jca	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ) → ( 𝑋 ∈ ℂHil ∧ ( Scalar ‘ 𝑋 ) = ℂfld ) )