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

Theorem phnv 21506
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 21505 . . 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 3465 . . 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 3284 . 2  |-  CPreHil OLD  C_  NrmCVec
43sseli 3252 1  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710   A.wral 2619    i^i cin 3227   ran crn 4772   ` cfv 5337  (class class class)co 5945   {coprab 5946   1c1 8828    + caddc 8830    x. cmul 8832   -ucneg 9128   2c2 9885   ^cexp 11197   NrmCVeccnv 21254   CPreHil OLDccphlo 21504
This theorem is referenced by:  phrel  21507  phnvi  21508  phop  21510  isph  21514  dipdi  21535  dipassr  21538  dipsubdir  21540  dipsubdi  21541  sspph  21547  ajval  21554  minvecolem1  21567  minvecolem2  21568  minvecolem3  21569  minvecolem4a  21570  minvecolem4b  21571  minvecolem4  21573  minvecolem5  21574  minvecolem6  21575  minvecolem7  21576
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242  df-ph 21505
  Copyright terms: Public domain W3C validator