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

Theorem phnvi 30835
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 𝑈 ∈ CPreHilOLD
Assertion
Ref Expression
phnvi 𝑈 ∈ NrmCVec

Proof of Theorem phnvi
StepHypRef Expression
1 phnvi.1 . 2 𝑈 ∈ CPreHilOLD
2 phnv 30833 . 2 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
31, 2ax-mp 5 1 𝑈 ∈ NrmCVec
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  NrmCVeccnv 30603  CPreHilOLDccphlo 30831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968  df-ph 30832
This theorem is referenced by:  elimph  30839  ip0i  30844  ip1ilem  30845  ip2i  30847  ipdirilem  30848  ipasslem1  30850  ipasslem2  30851  ipasslem4  30853  ipasslem5  30854  ipasslem7  30855  ipasslem8  30856  ipasslem9  30857  ipasslem10  30858  ipasslem11  30859  ip2dii  30863  pythi  30869  siilem1  30870  siilem2  30871  siii  30872  ipblnfi  30874  ip2eqi  30875  ajfuni  30878
  Copyright terms: Public domain W3C validator