MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  phnvi Unicode version

Theorem phnvi 22165
Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
Hypothesis
Ref Expression
phnvi.1  |-  U  e.  CPreHil
OLD
Assertion
Ref Expression
phnvi  |-  U  e.  NrmCVec

Proof of Theorem phnvi
StepHypRef Expression
1 phnvi.1 . 2  |-  U  e.  CPreHil
OLD
2 phnv 22163 . 2  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
31, 2ax-mp 8 1  |-  U  e.  NrmCVec
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   NrmCVeccnv 21911   CPreHil OLDccphlo 22161
This theorem is referenced by:  elimph  22169  ip0i  22174  ip1ilem  22175  ip2i  22177  ipdirilem  22178  ipasslem1  22180  ipasslem2  22181  ipasslem4  22183  ipasslem5  22184  ipasslem7  22185  ipasslem8  22186  ipasslem9  22187  ipasslem10  22188  ipasslem11  22189  ip2dii  22193  pythi  22199  siilem1  22200  siilem2  22201  siii  22202  ipblnfi  22205  ip2eqi  22206  ajfuni  22209
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277  df-ph 22162
  Copyright terms: Public domain W3C validator