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=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
Assertion	cnbn	$$⊢U\in \mathrm{CBan}$$

Proof

Step	Hyp	Ref	Expression
1		cnbn.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
2	1	cnnv	$$⊢U\in \mathrm{NrmCVec}$$
3		eqid	$$⊢⟨⟨+,\times ⟩,\mathrm{abs}⟩=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
4		eqid	$$⊢\mathrm{abs}\circ -=\mathrm{abs}\circ -$$
5	3 4	cnims	$$⊢\mathrm{abs}\circ -=\mathrm{IndMet}\left(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
6	5	eqcomi	$$⊢\mathrm{IndMet}\left(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)=\mathrm{abs}\circ -$$
7	6	cncmet	$$⊢\mathrm{IndMet}\left(⟨⟨+,\times ⟩,\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(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
10	9	eqcomi	$$⊢\mathrm{IndMet}\left(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)=\mathrm{IndMet}\left(U\right)$$
11	8 10	iscbn	$$⊢U\in \mathrm{CBan}\leftrightarrow \left(U\in \mathrm{NrmCVec}\wedge \mathrm{IndMet}\left(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\in \mathrm{CMet}\left(ℂ\right)\right)$$
12	2 7 11	mpbir2an	$$⊢U\in \mathrm{CBan}$$