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

Proof

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