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 ) )