Metamath Proof Explorer


Theorem chcompl

Description: Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion chcompl HCFCauchyF:HxHFvx

Proof

Step Hyp Ref Expression
1 isch3 HCHSfCauchyf:HxHfvx
2 1 simprbi HCfCauchyf:HxHfvx
3 feq1 f=Ff:HF:H
4 breq1 f=FfvxFvx
5 4 rexbidv f=FxHfvxxHFvx
6 3 5 imbi12d f=Ff:HxHfvxF:HxHFvx
7 6 rspccv fCauchyf:HxHfvxFCauchyF:HxHFvx
8 2 7 syl HCFCauchyF:HxHFvx
9 8 3imp HCFCauchyF:HxHFvx