Theorem phnv 31425

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 31424	. . 3 ⊢ CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔( -1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))})
2		inss1 4132	. . 3 ⊢ (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔( -1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))}) ⊆ NrmCVec
3	1, 2	eqsstri 3955	. 2 ⊢ CPreHilOLD ⊆ NrmCVec
4	3	sseli 3905	1 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ∩ cin 4088  ran crn 5652  ‘cfv 6543  (class class class)co 7424  {coprab 7425  1c1 11208   + caddc 11210   · cmul 11212   -cneg 11549  2c2 12404  ↑cexp 14211  NrmCVeccnv 31195  CPreHil_OLDccphlo 31423

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-in 4090  df-ph 31424

This theorem is used by:  phrel  31426  phnvi  31427  phop  31429  isph  31433  dipdi  31454  dipassr  31457  dipsubdir  31459  dipsubdi  31460  ajval  31472  minvecolem1  31485  minvecolem2  31486  minvecolem3  31487  minvecolem4a  31488  minvecolem4b  31489  minvecolem4  31491  minvecolem5  31492  minvecolem6  31493  minvecolem7  31494