Metamath Proof Explorer

Theorem cbncms

Description: The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007) Use bncmet (or preferably bncms ) instead. (New usage is discouraged.)

Ref Expression
Hypotheses iscbn.x ⊢ X = BaseSet ⁡ U
iscbn.8 ⊢ D = IndMet ⁡ U
Assertion cbncms ⊢ U ∈ CBan → D ∈ CMet ⁡ X

Proof

Step Hyp Ref Expression
1 iscbn.x ⊢ X = BaseSet ⁡ U
2 iscbn.8 ⊢ D = IndMet ⁡ U
3 1 2 iscbn ⊢ U ∈ CBan ↔ U ∈ NrmCVec ∧ D ∈ CMet ⁡ X
4 3 simprbi ⊢ U ∈ CBan → D ∈ CMet ⁡ X