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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	isbn	⊢ ( 𝑊 ∈ Ban ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ∧ 𝐹 ∈ CMetSp ) )

Proof

Step	Hyp	Ref	Expression
1		isbn.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		elin	⊢ ( 𝑊 ∈ ( NrmVec ∩ CMetSp ) ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ) )
3	2	anbi1i	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ CMetSp ) ∧ 𝐹 ∈ CMetSp ) ↔ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ) ∧ 𝐹 ∈ CMetSp ) )
4		fveq2	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
5	4 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
6	5	eleq1d	⊢ ( 𝑤 = 𝑊 → ( ( Scalar ‘ 𝑤 ) ∈ CMetSp ↔ 𝐹 ∈ CMetSp ) )
7		df-bn	⊢ Ban = { 𝑤 ∈ ( NrmVec ∩ CMetSp ) ∣ ( Scalar ‘ 𝑤 ) ∈ CMetSp }
8	6 7	elrab2	⊢ ( 𝑊 ∈ Ban ↔ ( 𝑊 ∈ ( NrmVec ∩ CMetSp ) ∧ 𝐹 ∈ CMetSp ) )
9		df-3an	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ∧ 𝐹 ∈ CMetSp ) ↔ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ) ∧ 𝐹 ∈ CMetSp ) )
10	3 8 9	3bitr4i	⊢ ( 𝑊 ∈ Ban ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ∧ 𝐹 ∈ CMetSp ) )