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	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )

Proof

Step	Hyp	Ref	Expression
1		df-ph	⊢ CPreHilOLD = ( NrmCVec ∩ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } )
2		inss1	⊢ ( NrmCVec ∩ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } ) ⊆ NrmCVec
3	1 2	eqsstri	⊢ CPreHilOLD ⊆ NrmCVec
4	3	sseli	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )