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

Theorem cphphl 25219
Description: A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
Assertion
Ref Expression
cphphl (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)

Proof of Theorem cphphl
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqid 2735 . . . 4 (Base‘𝑊) = (Base‘𝑊)
2 eqid 2735 . . . 4 (·𝑖𝑊) = (·𝑖𝑊)
3 eqid 2735 . . . 4 (norm‘𝑊) = (norm‘𝑊)
4 eqid 2735 . . . 4 (Scalar‘𝑊) = (Scalar‘𝑊)
5 eqid 2735 . . . 4 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
61, 2, 3, 4, 5iscph 25218 . . 3 (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂflds (Base‘(Scalar‘𝑊)))) ∧ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ∧ (norm‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (√‘(𝑥(·𝑖𝑊)𝑥)))))
76simp1bi 1144 . 2 (𝑊 ∈ ℂPreHil → (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂflds (Base‘(Scalar‘𝑊)))))
87simp1d 1141 1 (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1086   = wceq 1537  wcel 2106  cin 3962  wss 3963  cmpt 5231  cima 5692  cfv 6563  (class class class)co 7431  0cc0 11153  +∞cpnf 11290  [,)cico 13386  csqrt 15269  Basecbs 17245  s cress 17274  Scalarcsca 17301  ·𝑖cip 17303  fldccnfld 21382  PreHilcphl 21660  normcnm 24605  NrmModcnlm 24609  ℂPreHilccph 25214
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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5695  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fv 6571  df-ov 7434  df-cph 25216
This theorem is referenced by:  cphlvec  25223  cphcjcl  25231  cphipcl  25239  cphnmf  25243  cphipcj  25247  cphorthcom  25249  cphip0l  25250  cphip0r  25251  cphipeq0  25252  cphdir  25253  cphdi  25254  cph2di  25255  cphsubdir  25256  cphsubdi  25257  cph2subdi  25258  cphass  25259  cphassr  25260  ipcau  25286  nmparlem  25287  ipcn  25294  cphsscph  25299  hlphl  25413  cmscsscms  25421  bncssbn  25422  pjthlem2  25486
  Copyright terms: Public domain W3C validator