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

Theorem cphphl 18705
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 2358 . . . 4  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2358 . . . 4  |-  ( .i
`  W )  =  ( .i `  W
)
3 eqid 2358 . . . 4  |-  ( norm `  W )  =  (
norm `  W )
4 eqid 2358 . . . 4  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2358 . . . 4  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
61, 2, 3, 4, 5iscph 18704 . . 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 970 . 2  |-  ( W  e.  CPreHil  ->  ( W  e. 
PreHil  /\  W  e. NrmMod  /\  (Scalar `  W )  =  (flds  ( Base `  (Scalar `  W )
) ) ) )
87simp1d 967 1  |-  ( W  e.  CPreHil  ->  W  e.  PreHil )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    = wceq 1642    e. wcel 1710    i^i cin 3227    C_ wss 3228    e. cmpt 4156   "cima 4771   ` cfv 5334  (class class class)co 5942   0cc0 8824    +oocpnf 8951   [,)cico 10747   sqrcsqr 11808   Basecbs 13239   ↾s cress 13240  Scalarcsca 13302   .icip 13304  ℂfldccnfld 16476   PreHilcphl 16628   normcnm 18195  NrmModcnlm 18199   CPreHilccph 18700
This theorem is referenced by:  cphlvec  18709  cphcjcl  18717  cphipcl  18725  cphnmf  18729  cphipcj  18733  cphorthcom  18734  cphip0l  18735  cphip0r  18736  cphipeq0  18737  cphdir  18738  cphdi  18739  cph2di  18740  cphsubdir  18741  cphsubdi  18742  cph2subdi  18743  cphass  18744  cphassr  18745  ipcau  18766  nmparlem  18767  ipcn  18771  hlphl  18880  pjthlem2  18900
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-nul 4228
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-mpt 4158  df-xp 4774  df-cnv 4776  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fv 5342  df-ov 5945  df-cph 18702
  Copyright terms: Public domain W3C validator