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

Theorem phnv 24236
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 24235 . . 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 3591 . . 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 3407 . 2  |-  CPreHil OLD  C_  NrmCVec
43sseli 3373 1  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   A.wral 2736    i^i cin 3348   ran crn 4862   ` cfv 5439  (class class class)co 6112   {coprab 6113   1c1 9304    + caddc 9306    x. cmul 9308   -ucneg 9617   2c2 10392   ^cexp 11886   NrmCVeccnv 23984   CPreHil OLDccphlo 24234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363  df-ph 24235
This theorem is referenced by:  phrel  24237  phnvi  24238  phop  24240  isph  24244  dipdi  24265  dipassr  24268  dipsubdir  24270  dipsubdi  24271  sspph  24277  ajval  24284  minvecolem1  24297  minvecolem2  24298  minvecolem3  24299  minvecolem4a  24300  minvecolem4b  24301  minvecolem4  24303  minvecolem5  24304  minvecolem6  24305  minvecolem7  24306
  Copyright terms: Public domain W3C validator