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

Theorem phnv 21392
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  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )

Proof of Theorem phnv
Dummy variables  g  n  s  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ph 21391 . . 3  |-  CPreHil OLD  =  ( NrmCVec  i^i  { <. <. g ,  s >. ,  n >.  |  A. x  e. 
ran  g A. y  e.  ran  g ( ( ( n `  (
x g y ) ) ^ 2 )  +  ( ( n `
 ( x g ( -u 1 s y ) ) ) ^ 2 ) )  =  ( 2  x.  ( ( ( n `
 x ) ^
2 )  +  ( ( n `  y
) ^ 2 ) ) ) } )
2 inss1 3389 . . 3  |-  ( NrmCVec  i^i 
{ <. <. g ,  s
>. ,  n >.  | 
A. x  e.  ran  g A. y  e.  ran  g ( ( ( n `  ( x g y ) ) ^ 2 )  +  ( ( n `  ( x g (
-u 1 s y ) ) ) ^
2 ) )  =  ( 2  x.  (
( ( n `  x ) ^ 2 )  +  ( ( n `  y ) ^ 2 ) ) ) } )  C_  NrmCVec
31, 2eqsstri 3208 . 2  |-  CPreHil OLD  C_  NrmCVec
43sseli 3176 1  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   A.wral 2543    i^i cin 3151   ran crn 4690   ` cfv 5255  (class class class)co 5858   {coprab 5859   1c1 8738    + caddc 8740    x. cmul 8742   -ucneg 9038   2c2 9795   ^cexp 11104   NrmCVeccnv 21140   CPreHil OLDccphlo 21390
This theorem is referenced by:  phrel  21393  phnvi  21394  phop  21396  isph  21400  dipdi  21421  dipassr  21424  dipsubdir  21426  dipsubdi  21427  sspph  21433  ajval  21440  minvecolem1  21453  minvecolem2  21454  minvecolem3  21455  minvecolem4a  21456  minvecolem4b  21457  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  minvecolem7  21462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-ph 21391
  Copyright terms: Public domain W3C validator