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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	bnsca	⊢ ( 𝑊 ∈ Ban → 𝐹 ∈ CMetSp )

Proof

Step	Hyp	Ref	Expression
1		isbn.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2	1	isbn	⊢ ( 𝑊 ∈ Ban ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ∧ 𝐹 ∈ CMetSp ) )
3	2	simp3bi	⊢ ( 𝑊 ∈ Ban → 𝐹 ∈ CMetSp )