MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cphphl Structured version   Unicode version

Theorem cphphl 21910
Description: A complex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
Assertion
Ref Expression
cphphl  |-  ( W  e.  CPreHil  ->  W  e.  PreHil )

Proof of Theorem cphphl
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqid 2402 . . . 4  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2402 . . . 4  |-  ( .i
`  W )  =  ( .i `  W
)
3 eqid 2402 . . . 4  |-  ( norm `  W )  =  (
norm `  W )
4 eqid 2402 . . . 4  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2402 . . . 4  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
61, 2, 3, 4, 5iscph 21909 . . 3  |-  ( W  e.  CPreHil 
<->  ( ( W  e. 
PreHil  /\  W  e. NrmMod  /\  (Scalar `  W )  =  (flds  ( Base `  (Scalar `  W )
) ) )  /\  ( sqr " ( (
Base `  (Scalar `  W
) )  i^i  (
0 [,) +oo )
) )  C_  ( Base `  (Scalar `  W
) )  /\  ( norm `  W )  =  ( x  e.  (
Base `  W )  |->  ( sqr `  (
x ( .i `  W ) x ) ) ) ) )
76simp1bi 1012 . 2  |-  ( W  e.  CPreHil  ->  ( W  e. 
PreHil  /\  W  e. NrmMod  /\  (Scalar `  W )  =  (flds  ( Base `  (Scalar `  W )
) ) ) )
87simp1d 1009 1  |-  ( W  e.  CPreHil  ->  W  e.  PreHil )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974    = wceq 1405    e. wcel 1842    i^i cin 3413    C_ wss 3414    |-> cmpt 4453   "cima 4826   ` cfv 5569  (class class class)co 6278   0cc0 9522   +oocpnf 9655   [,)cico 11584   sqrcsqrt 13215   Basecbs 14841   ↾s cress 14842  Scalarcsca 14912   .icip 14914  ℂfldccnfld 18740   PreHilcphl 18957   normcnm 21389  NrmModcnlm 21393   CPreHilccph 21905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-nul 4525
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-mpt 4455  df-xp 4829  df-cnv 4831  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fv 5577  df-ov 6281  df-cph 21907
This theorem is referenced by:  cphlvec  21914  cphcjcl  21922  cphipcl  21930  cphnmf  21934  cphipcj  21938  cphorthcom  21939  cphip0l  21940  cphip0r  21941  cphipeq0  21942  cphdir  21943  cphdi  21944  cph2di  21945  cphsubdir  21946  cphsubdi  21947  cph2subdi  21948  cphass  21949  cphassr  21950  ipcau  21973  nmparlem  21974  ipcn  21978  hlphl  22097  pjthlem2  22145
  Copyright terms: Public domain W3C validator