Theorem phnv 27669

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.

Step	Hyp	Ref	Expression
1		df-ph 27668	. . 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 3833	. . 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
3	1, 2	eqsstri 3635	. 2 |- CPreHil OLD C_ NrmCVec
4	3	sseli 3599	1 |- ( U e. CPreHil OLD -> U e. NrmCVec )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   A.wral 2912   i^i cin 3573   ran crn 5115   ` cfv 5888  (class class class)co 6650   {coprab 6651   1c1 9937   + caddc 9939   x. cmul 9941   -ucneg 10267   2c2 11070   ^cexp 12860   NrmCVeccnv 27439   CPreHil OLDccphlo 27667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-ph 27668

This theorem is referenced by:  phrel  27670  phnvi  27671  phop  27673  isph  27677  dipdi  27698  dipassr  27701  dipsubdir  27703  dipsubdi  27704  sspph  27710  ajval  27717  minvecolem1  27730  minvecolem2  27731  minvecolem3  27732  minvecolem4a  27733  minvecolem4b  27734  minvecolem4  27736  minvecolem5  27737  minvecolem6  27738  minvecolem7  27739