Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  phnv Structured version   Visualization version   GIF version

Theorem phnv 28585
 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.
StepHypRef Expression
1 df-ph 28584 . . 3 CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
2 inss1 4204 . . 3 (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))}) ⊆ NrmCVec
31, 2eqsstri 4000 . 2 CPreHilOLD ⊆ NrmCVec
43sseli 3962 1 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  ∀wral 3138   ∩ cin 3934  ran crn 5550  ‘cfv 6349  (class class class)co 7150  {coprab 7151  1c1 10532   + caddc 10534   · cmul 10536  -cneg 10865  2c2 11686  ↑cexp 13423  NrmCVeccnv 28355  CPreHilOLDccphlo 28583 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951  df-ph 28584 This theorem is referenced by:  phrel  28586  phnvi  28587  phop  28589  isph  28593  dipdi  28614  dipassr  28617  dipsubdir  28619  dipsubdi  28620  ajval  28632  minvecolem1  28645  minvecolem2  28646  minvecolem3  28647  minvecolem4a  28648  minvecolem4b  28649  minvecolem4  28651  minvecolem5  28652  minvecolem6  28653  minvecolem7  28654
 Copyright terms: Public domain W3C validator