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 e. CBan -> D e. ( CMet ` X ) )

Proof

Step Hyp Ref Expression
1 iscbn.x
 |-  X = ( BaseSet ` U )
2 iscbn.8
 |-  D = ( IndMet ` U )
3 1 2 iscbn
 |-  ( U e. CBan <-> ( U e. NrmCVec /\ D e. ( CMet ` X ) ) )
4 3 simprbi
 |-  ( U e. CBan -> D e. ( CMet ` X ) )