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

Theorem phnvi 21410
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 21408 . 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 1696   NrmCVeccnv 21156   CPreHil OLDccphlo 21406
This theorem is referenced by:  elimph  21414  ip0i  21419  ip1ilem  21420  ip2i  21422  ipdirilem  21423  ipasslem1  21425  ipasslem2  21426  ipasslem4  21428  ipasslem5  21429  ipasslem7  21430  ipasslem8  21431  ipasslem9  21432  ipasslem10  21433  ipasslem11  21434  ip2dii  21438  pythi  21444  siilem1  21445  siilem2  21446  siii  21447  ipblnfi  21450  ip2eqi  21451  ajfuni  21454
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-ph 21407
  Copyright terms: Public domain W3C validator