Metamath Proof Explorer

Theorem isbn

Description: A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Hypothesis	isbn.1	$⊢ F = Scalar (W)$
	Assertion	isbn	$⊢ W \in Ban \leftrightarrow (W \in NrmVec \land W \in CMetSp \land F \in CMetSp)$

Proof

Step	Hyp	Ref	Expression
1		isbn.1	$⊢ F = Scalar (W)$
2		elin	$⊢ W \in (NrmVec \cap CMetSp) \leftrightarrow (W \in NrmVec \land W \in CMetSp)$
3	2	anbi1i	$⊢ (W \in (NrmVec \cap CMetSp) \land F \in CMetSp) \leftrightarrow ((W \in NrmVec \land W \in CMetSp) \land F \in CMetSp)$
4		fveq2	$⊢ w = W \to Scalar (w) = Scalar (W)$
5	4 1	eqtr4di	$⊢ w = W \to Scalar (w) = F$
6	5	eleq1d	$⊢ w = W \to (Scalar (w) \in CMetSp \leftrightarrow F \in CMetSp)$
7		df-bn	$⊢ Ban = \{w \in (NrmVec \cap CMetSp) \| Scalar (w) \in CMetSp\}$
8	6 7	elrab2	$⊢ W \in Ban \leftrightarrow (W \in (NrmVec \cap CMetSp) \land F \in CMetSp)$
9		df-3an	$⊢ (W \in NrmVec \land W \in CMetSp \land F \in CMetSp) \leftrightarrow ((W \in NrmVec \land W \in CMetSp) \land F \in CMetSp)$
10	3 8 9	3bitr4i	$⊢ W \in Ban \leftrightarrow (W \in NrmVec \land W \in CMetSp \land F \in CMetSp)$