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 𝐹 = ( 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 ) )