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

Theorem phnvi 25404
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 25402 . 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 1767   NrmCVeccnv 25150   CPreHil OLDccphlo 25400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-ph 25401
This theorem is referenced by:  elimph  25408  ip0i  25413  ip1ilem  25414  ip2i  25416  ipdirilem  25417  ipasslem1  25419  ipasslem2  25420  ipasslem4  25422  ipasslem5  25423  ipasslem7  25424  ipasslem8  25425  ipasslem9  25426  ipasslem10  25427  ipasslem11  25428  ip2dii  25432  pythi  25438  siilem1  25439  siilem2  25440  siii  25441  ipblnfi  25444  ip2eqi  25445  ajfuni  25448
  Copyright terms: Public domain W3C validator