Theorem phnv 31416

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

Assertion

Ref	Expression
phnv	⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec)

Proof of Theorem phnv

Dummy variables 𝑔 𝑛 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3077   ∩ cin 3898  ran crn 5652  ‘cfv 6538  (class class class)co 7420  {coprab 7421  1c1 11201   + caddc 11203   · cmul 11205  -cneg 11542  2c2 12397  ↑cexp 14204  NrmCVeccnv 31186  CPreHil_OLDccphlo 31414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916  df-ph 31415

This theorem is used by:  phrel  31417  phnvi  31418  phop  31420  isph  31424  dipdi  31445  dipassr  31448  dipsubdir  31450  dipsubdi  31451  ajval  31463  minvecolem1  31476  minvecolem2  31477  minvecolem3  31478  minvecolem4a  31479  minvecolem4b  31480  minvecolem4  31482  minvecolem5  31483  minvecolem6  31484  minvecolem7  31485