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

Theorem phnvi 26145
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 26143 . 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 1842   NrmCVeccnv 25891   CPreHil OLDccphlo 26141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-in 3421  df-ss 3428  df-ph 26142
This theorem is referenced by:  elimph  26149  ip0i  26154  ip1ilem  26155  ip2i  26157  ipdirilem  26158  ipasslem1  26160  ipasslem2  26161  ipasslem4  26163  ipasslem5  26164  ipasslem7  26165  ipasslem8  26166  ipasslem9  26167  ipasslem10  26168  ipasslem11  26169  ip2dii  26173  pythi  26179  siilem1  26180  siilem2  26181  siii  26182  ipblnfi  26185  ip2eqi  26186  ajfuni  26189
  Copyright terms: Public domain W3C validator