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

Theorem phnv 22353
 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 22352 . . 3
2 inss1 3549 . . 3
31, 2eqsstri 3367 . 2
43sseli 3333 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1654   wcel 1728  wral 2712   cin 3308   crn 4914  cfv 5489  (class class class)co 6117  coprab 6118  c1 9029   caddc 9031   cmul 9033  cneg 9330  c2 10087  cexp 11420  cnv 22101  ccphlo 22351 This theorem is referenced by:  phrel  22354  phnvi  22355  phop  22357  isph  22361  dipdi  22382  dipassr  22385  dipsubdir  22387  dipsubdi  22388  sspph  22394  ajval  22401  minvecolem1  22414  minvecolem2  22415  minvecolem3  22416  minvecolem4a  22417  minvecolem4b  22418  minvecolem4  22420  minvecolem5  22421  minvecolem6  22422  minvecolem7  22423 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2967  df-in 3316  df-ss 3323  df-ph 22352
 Copyright terms: Public domain W3C validator