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

Theorem cphphl 22142
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 2450 . . . 4  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2450 . . . 4  |-  ( .i
`  W )  =  ( .i `  W
)
3 eqid 2450 . . . 4  |-  ( norm `  W )  =  (
norm `  W )
4 eqid 2450 . . . 4  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2450 . . . 4  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
61, 2, 3, 4, 5iscph 22141 . . 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 1022 . 2  |-  ( W  e.  CPreHil  ->  ( W  e. 
PreHil  /\  W  e. NrmMod  /\  (Scalar `  W )  =  (flds  ( Base `  (Scalar `  W )
) ) ) )
87simp1d 1019 1  |-  ( W  e.  CPreHil  ->  W  e.  PreHil )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 984    = wceq 1443    e. wcel 1886    i^i cin 3402    C_ wss 3403    |-> cmpt 4460   "cima 4836   ` cfv 5581  (class class class)co 6288   0cc0 9536   +oocpnf 9669   [,)cico 11634   sqrcsqrt 13289   Basecbs 15114   ↾s cress 15115  Scalarcsca 15186   .icip 15188  ℂfldccnfld 18963   PreHilcphl 19184   normcnm 21584  NrmModcnlm 21588   CPreHilccph 22137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-nul 4533
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-xp 4839  df-cnv 4841  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fv 5589  df-ov 6291  df-cph 22139
This theorem is referenced by:  cphlvec  22146  cphcjcl  22154  cphipcl  22162  cphnmf  22166  cphipcj  22170  cphorthcom  22171  cphip0l  22172  cphip0r  22173  cphipeq0  22174  cphdir  22175  cphdi  22176  cph2di  22177  cphsubdir  22178  cphsubdi  22179  cph2subdi  22180  cphass  22181  cphassr  22182  ipcau  22205  nmparlem  22206  ipcn  22210  hlphl  22325  pjthlem2  22385
  Copyright terms: Public domain W3C validator