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 𝑋 = ( BaseSet ‘ 𝑈 )
iscbn.8 𝐷 = ( IndMet ‘ 𝑈 )
Assertion iscbn ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 iscbn.x 𝑋 = ( BaseSet ‘ 𝑈 )
2 iscbn.8 𝐷 = ( IndMet ‘ 𝑈 )
3 fveq2 ( 𝑢 = 𝑈 → ( IndMet ‘ 𝑢 ) = ( IndMet ‘ 𝑈 ) )
4 3 2 eqtr4di ( 𝑢 = 𝑈 → ( IndMet ‘ 𝑢 ) = 𝐷 )
5 fveq2 ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
6 5 1 eqtr4di ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
7 6 fveq2d ( 𝑢 = 𝑈 → ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) = ( CMet ‘ 𝑋 ) )
8 4 7 eleq12d ( 𝑢 = 𝑈 → ( ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) ↔ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )
9 df-cbn CBan = { 𝑢 ∈ NrmCVec ∣ ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) }
10 8 9 elrab2 ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )