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

Theorem phnv 22276
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 22275 . . 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 3529 . . 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 3346 . 2  |-  CPreHil OLD  C_  NrmCVec
43sseli 3312 1  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   A.wral 2674    i^i cin 3287   ran crn 4846   ` cfv 5421  (class class class)co 6048   {coprab 6049   1c1 8955    + caddc 8957    x. cmul 8959   -ucneg 9256   2c2 10013   ^cexp 11345   NrmCVeccnv 22024   CPreHil OLDccphlo 22274
This theorem is referenced by:  phrel  22277  phnvi  22278  phop  22280  isph  22284  dipdi  22305  dipassr  22308  dipsubdir  22310  dipsubdi  22311  sspph  22317  ajval  22324  minvecolem1  22337  minvecolem2  22338  minvecolem3  22339  minvecolem4a  22340  minvecolem4b  22341  minvecolem4  22343  minvecolem5  22344  minvecolem6  22345  minvecolem7  22346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295  df-ss 3302  df-ph 22275
  Copyright terms: Public domain W3C validator