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

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 ⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , 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