Metamath Proof Explorer

Theorem iscbn

Description: A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006) Use isbn instead. (New usage is discouraged.)

Ref Expression
Hypotheses iscbn.x ⊢ X = BaseSet ⁡ U
iscbn.8 ⊢ D = IndMet ⁡ U
Assertion iscbn ⊢ U ∈ CBan ↔ U ∈ NrmCVec ∧ D ∈ CMet ⁡ X

Proof

Step Hyp Ref Expression
1 iscbn.x ⊢ X = BaseSet ⁡ U
2 iscbn.8 ⊢ D = IndMet ⁡ U
3 fveq2 ⊢ u = U → IndMet ⁡ u = IndMet ⁡ U
4 3 2 eqtr4di ⊢ u = U → IndMet ⁡ u = D
5 fveq2 ⊢ u = U → BaseSet ⁡ u = BaseSet ⁡ U
6 5 1 eqtr4di ⊢ u = U → BaseSet ⁡ u = X
7 6 fveq2d ⊢ u = U → CMet ⁡ BaseSet ⁡ u = CMet ⁡ X
8 4 7 eleq12d ⊢ u = U → IndMet ⁡ u ∈ CMet ⁡ BaseSet ⁡ u ↔ D ∈ CMet ⁡ X
9 df-cbn ⊢ CBan = u ∈ NrmCVec | IndMet ⁡ u ∈ CMet ⁡ BaseSet ⁡ u
10 8 9 elrab2 ⊢ U ∈ CBan ↔ U ∈ NrmCVec ∧ D ∈ CMet ⁡ X