This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )