Metamath Proof Explorer

Theorem bnsca

Description: The scalar field of a Banach space is complete. (Contributed by NM, 8-Sep-2007) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis isbn.1 
|- F = ( Scalar ` W )
Assertion bnsca 
|- ( W e. Ban -> F e. CMetSp )

Proof

Step Hyp Ref Expression
1 isbn.1 
 |-  F = ( Scalar ` W )
2 1 isbn 
 |-  ( W e. Ban <-> ( W e. NrmVec /\ W e. CMetSp /\ F e. CMetSp ) )
3 2 simp3bi 
 |-  ( W e. Ban -> F e. CMetSp )