MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bnnv Structured version   Visualization version   GIF version

Theorem bnnv 29236
Description: Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 24514 instead. (New usage is discouraged.)
Assertion
Ref Expression
bnnv (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)

Proof of Theorem bnnv
StepHypRef Expression
1 eqid 2738 . . 3 (BaseSet‘𝑈) = (BaseSet‘𝑈)
2 eqid 2738 . . 3 (IndMet‘𝑈) = (IndMet‘𝑈)
31, 2iscbn 29234 . 2 (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ (IndMet‘𝑈) ∈ (CMet‘(BaseSet‘𝑈))))
43simplbi 498 1 (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  cfv 6426  CMetccmet 24428  NrmCVeccnv 28954  BaseSetcba 28956  IndMetcims 28961  CBanccbn 29232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3431  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5074  df-iota 6384  df-fv 6434  df-cbn 29233
This theorem is referenced by:  bnrel  29237  bnsscmcl  29238  ubthlem1  29240  ubthlem2  29241  ubthlem3  29242  minvecolem1  29244  hlnv  29261
  Copyright terms: Public domain W3C validator