This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
|
Assertion |
bnsca |
⊢ ( 𝑊 ∈ Ban → 𝐹 ∈ CMetSp ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isbn.1 |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
| 2 |
1
|
isbn |
⊢ ( 𝑊 ∈ Ban ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ∧ 𝐹 ∈ CMetSp ) ) |
| 3 |
2
|
simp3bi |
⊢ ( 𝑊 ∈ Ban → 𝐹 ∈ CMetSp ) |