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 \in {CPreHil}_{OLD} \to U \in NrmCVec$

Step	Hyp	Ref	Expression
1		df-ph	$⊢ {CPreHil}_{OLD} = NrmCVec \cap \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\}$
2		inss1	$⊢ NrmCVec \cap \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\} \subseteq NrmCVec$
3	1 2	eqsstri	$⊢ {CPreHil}_{OLD} \subseteq NrmCVec$
4	3	sseli	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$

Metamath Proof Explorer