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

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 ) )