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

Theorem phnv 26300
 Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
phnv

Proof of Theorem phnv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ph 26299 . . 3
2 inss1 3688 . . 3
31, 2eqsstri 3500 . 2
43sseli 3466 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1437   wcel 1870  wral 2782   cin 3441   crn 4855  cfv 5601  (class class class)co 6305  coprab 6306  c1 9539   caddc 9541   cmul 9543  cneg 9860  c2 10659  cexp 12269  cnv 26048  ccphlo 26298 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456  df-ph 26299 This theorem is referenced by:  phrel  26301  phnvi  26302  phop  26304  isph  26308  dipdi  26329  dipassr  26332  dipsubdir  26334  dipsubdi  26335  sspph  26341  ajval  26348  minvecolem1  26361  minvecolem2  26362  minvecolem3  26363  minvecolem4a  26364  minvecolem4b  26365  minvecolem4  26367  minvecolem5  26368  minvecolem6  26369  minvecolem7  26370
 Copyright terms: Public domain W3C validator