This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED) Complex Banach spaces Definition and basic properties 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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
iscbn.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion
cbncms ⊢ ( 𝑈 ∈ CBan → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
Proof
Step
Hyp
Ref
Expression
1
iscbn.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2
iscbn.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3
1 2
iscbn ⊢ ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )
4
3
simprbi ⊢ ( 𝑈 ∈ CBan → 𝐷 ∈ ( CMet ‘ 𝑋 ) )