MPE Home 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  |-  ( 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 22352 . . 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 3549 . . 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 3367 . 2  |-  CPreHil OLD  C_  NrmCVec
43sseli 3333 1  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1654    e. wcel 1728   A.wral 2712    i^i cin 3308   ran crn 4914   ` cfv 5489  (class class class)co 6117   {coprab 6118   1c1 9029    + caddc 9031    x. cmul 9033   -ucneg 9330   2c2 10087   ^cexp 11420   NrmCVeccnv 22101   CPreHil OLDccphlo 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