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

Theorem phnvi 22309
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 22307 . 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 1725   NrmCVeccnv 22055   CPreHil OLDccphlo 22305
This theorem is referenced by:  elimph  22313  ip0i  22318  ip1ilem  22319  ip2i  22321  ipdirilem  22322  ipasslem1  22324  ipasslem2  22325  ipasslem4  22327  ipasslem5  22328  ipasslem7  22329  ipasslem8  22330  ipasslem9  22331  ipasslem10  22332  ipasslem11  22333  ip2dii  22337  pythi  22343  siilem1  22344  siilem2  22345  siii  22346  ipblnfi  22349  ip2eqi  22350  ajfuni  22353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-ph 22306
  Copyright terms: Public domain W3C validator