Theorem phnv

Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	phnv	|- ( U e. CPreHilOLD -> U e. NrmCVec )

Proof

Step	Hyp	Ref	Expression
1		df-ph	|- CPreHilOLD = ( 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	|- ( 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	|- CPreHilOLD C_ NrmCVec
4	3	sseli	|- ( U e. CPreHilOLD -> U e. NrmCVec )