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	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
Assertion	cnbn	⊢ 𝑈 ∈ CBan

Proof

Step	Hyp	Ref	Expression
1		cnbn.6	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2	1	cnnv	⊢ 𝑈 ∈ NrmCVec
3		eqid	⊢ ⟨ ⟨ + , · ⟩ , abs ⟩ = ⟨ ⟨ + , · ⟩ , abs ⟩
4		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
5	3 4	cnims	⊢ ( abs ∘ − ) = ( IndMet ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ )
6	5	eqcomi	⊢ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ ) = ( abs ∘ − )
7	6	cncmet	⊢ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ ( CMet ‘ ℂ )
8	1	cnnvba	⊢ ℂ = ( BaseSet ‘ 𝑈 )
9	1	fveq2i	⊢ ( IndMet ‘ 𝑈 ) = ( IndMet ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ )
10	9	eqcomi	⊢ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ ) = ( IndMet ‘ 𝑈 )
11	8 10	iscbn	⊢ ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ ( CMet ‘ ℂ ) ) )
12	2 7 11	mpbir2an	⊢ 𝑈 ∈ CBan