This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Ban \to F \in CMetSp$

Step	Hyp	Ref	Expression
1		isbn.1	$⊢ F = Scalar (W)$
2	1	isbn	$⊢ W \in Ban \leftrightarrow (W \in NrmVec \land W \in CMetSp \land F \in CMetSp)$
3	2	simp3bi	$⊢ W \in Ban \to F \in CMetSp$