# Metamath Proof Explorer

## Theorem cnbn

Description: The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007) (New usage is discouraged.)

Ref Expression
Hypothesis cnbn.6 ${⊢}{U}=⟨⟨+,×⟩,\mathrm{abs}⟩$
Assertion cnbn ${⊢}{U}\in \mathrm{CBan}$

### Proof

Step Hyp Ref Expression
1 cnbn.6 ${⊢}{U}=⟨⟨+,×⟩,\mathrm{abs}⟩$
2 1 cnnv ${⊢}{U}\in \mathrm{NrmCVec}$
3 eqid ${⊢}⟨⟨+,×⟩,\mathrm{abs}⟩=⟨⟨+,×⟩,\mathrm{abs}⟩$
4 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
5 3 4 cnims ${⊢}\mathrm{abs}\circ -=\mathrm{IndMet}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
6 5 eqcomi ${⊢}\mathrm{IndMet}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)=\mathrm{abs}\circ -$
7 6 cncmet ${⊢}\mathrm{IndMet}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)\in \mathrm{CMet}\left(ℂ\right)$
8 1 cnnvba ${⊢}ℂ=\mathrm{BaseSet}\left({U}\right)$
9 1 fveq2i ${⊢}\mathrm{IndMet}\left({U}\right)=\mathrm{IndMet}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
10 9 eqcomi ${⊢}\mathrm{IndMet}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)=\mathrm{IndMet}\left({U}\right)$
11 8 10 iscbn ${⊢}{U}\in \mathrm{CBan}↔\left({U}\in \mathrm{NrmCVec}\wedge \mathrm{IndMet}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)\in \mathrm{CMet}\left(ℂ\right)\right)$
12 2 7 11 mpbir2an ${⊢}{U}\in \mathrm{CBan}$