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

Theorem phnv 30067
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 30066 . . 3 CPreHilOLD = (NrmCVec โˆฉ {โŸจโŸจ๐‘”, ๐‘ โŸฉ, ๐‘›โŸฉ โˆฃ โˆ€๐‘ฅ โˆˆ ran ๐‘”โˆ€๐‘ฆ โˆˆ ran ๐‘”(((๐‘›โ€˜(๐‘ฅ๐‘”๐‘ฆ))โ†‘2) + ((๐‘›โ€˜(๐‘ฅ๐‘”(-1๐‘ ๐‘ฆ)))โ†‘2)) = (2 ยท (((๐‘›โ€˜๐‘ฅ)โ†‘2) + ((๐‘›โ€˜๐‘ฆ)โ†‘2)))})
2 inss1 4229 . . 3 (NrmCVec โˆฉ {โŸจโŸจ๐‘”, ๐‘ โŸฉ, ๐‘›โŸฉ โˆฃ โˆ€๐‘ฅ โˆˆ ran ๐‘”โˆ€๐‘ฆ โˆˆ ran ๐‘”(((๐‘›โ€˜(๐‘ฅ๐‘”๐‘ฆ))โ†‘2) + ((๐‘›โ€˜(๐‘ฅ๐‘”(-1๐‘ ๐‘ฆ)))โ†‘2)) = (2 ยท (((๐‘›โ€˜๐‘ฅ)โ†‘2) + ((๐‘›โ€˜๐‘ฆ)โ†‘2)))}) โŠ† NrmCVec
31, 2eqsstri 4017 . 2 CPreHilOLD โŠ† NrmCVec
43sseli 3979 1 (๐‘ˆ โˆˆ CPreHilOLD โ†’ ๐‘ˆ โˆˆ NrmCVec)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3062   โˆฉ cin 3948  ran crn 5678  โ€˜cfv 6544  (class class class)co 7409  {coprab 7410  1c1 11111   + caddc 11113   ยท cmul 11115  -cneg 11445  2c2 12267  โ†‘cexp 14027  NrmCVeccnv 29837  CPreHilOLDccphlo 30065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-ph 30066
This theorem is referenced by:  phrel  30068  phnvi  30069  phop  30071  isph  30075  dipdi  30096  dipassr  30099  dipsubdir  30101  dipsubdi  30102  ajval  30114  minvecolem1  30127  minvecolem2  30128  minvecolem3  30129  minvecolem4a  30130  minvecolem4b  30131  minvecolem4  30133  minvecolem5  30134  minvecolem6  30135  minvecolem7  30136
  Copyright terms: Public domain W3C validator