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

Theorem phnvi 24363
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 24361 . 2  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
31, 2ax-mp 5 1  |-  U  e.  NrmCVec
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   NrmCVeccnv 24109   CPreHil OLDccphlo 24359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-v 3074  df-in 3438  df-ss 3445  df-ph 24360
This theorem is referenced by:  elimph  24367  ip0i  24372  ip1ilem  24373  ip2i  24375  ipdirilem  24376  ipasslem1  24378  ipasslem2  24379  ipasslem4  24381  ipasslem5  24382  ipasslem7  24383  ipasslem8  24384  ipasslem9  24385  ipasslem10  24386  ipasslem11  24387  ip2dii  24391  pythi  24397  siilem1  24398  siilem2  24399  siii  24400  ipblnfi  24403  ip2eqi  24404  ajfuni  24407
  Copyright terms: Public domain W3C validator