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