Theorem cphphl 25099

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.

Step	Hyp	Ref	Expression
1		eqid 2733	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2733	. . . 4 ⊢ (·𝑖‘𝑊) = (·𝑖‘𝑊)
3		eqid 2733	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
4		eqid 2733	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2733	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6	1, 2, 3, 4, 5	iscph 25098	. . 3 ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊)))) ∧ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ∧ (norm‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (√‘(𝑥(·𝑖‘𝑊)𝑥)))))
7	6	simp1bi 1145	. 2 ⊢ (𝑊 ∈ ℂPreHil → (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊)))))
8	7	simp1d 1142	1 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ∩ cin 3897   ⊆ wss 3898   ↦ cmpt 5174   “ cima 5622  ‘cfv 6486  (class class class)co 7352  0cc0 11013  +∞cpnf 11150  [,)cico 13249  √csqrt 15142  Basecbs 17122   ↾_s cress 17143  Scalarcsca 17166  ·_𝑖cip 17168  ℂ_fldccnfld 21293  PreHilcphl 21563  normcnm 24492  NrmModcnlm 24496  ℂPreHilccph 25094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fv 6494  df-ov 7355  df-cph 25096

This theorem is referenced by:  cphlvec  25103  cphcjcl  25111  cphipcl  25119  cphnmf  25123  cphipcj  25127  cphorthcom  25129  cphip0l  25130  cphip0r  25131  cphipeq0  25132  cphdir  25133  cphdi  25134  cph2di  25135  cphsubdir  25136  cphsubdi  25137  cph2subdi  25138  cphass  25139  cphassr  25140  ipcau  25166  nmparlem  25167  ipcn  25174  cphsscph  25179  hlphl  25293  cmscsscms  25301  bncssbn  25302  pjthlem2  25366