Theorem cphphl 25163

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 2740	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2740	. . . 4 ⊢ (·𝑖‘𝑊) = (·𝑖‘𝑊)
3		eqid 2740	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
4		eqid 2740	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2740	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6	1, 2, 3, 4, 5	iscph 25162	. . 3 ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊)))) ∧ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ∧ (norm‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (√‘(𝑥(·𝑖‘𝑊)𝑥)))))
7	6	simp1bi 1151	. 2 ⊢ (𝑊 ∈ ℂPreHil → (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊)))))
8	7	simp1d 1148	1 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ∩ cin 3889   ⊆ wss 3890   ↦ cmpt 5160   “ cima 5628  ‘cfv 6492  (class class class)co 7363  0cc0 11036  +∞cpnf 11174  [,)cico 13298  √csqrt 15193  Basecbs 17177   ↾_s cress 17198  Scalarcsca 17221  ·_𝑖cip 17223  ℂ_fldccnfld 21354  PreHilcphl 21606  normcnm 24566  NrmModcnlm 24570  ℂPreHilccph 25158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fv 6500  df-ov 7366  df-cph 25160

This theorem is referenced by:  cphlvec  25167  cphcjcl  25175  cphipcl  25183  cphnmf  25187  cphipcj  25191  cphorthcom  25193  cphip0l  25194  cphip0r  25195  cphipeq0  25196  cphdir  25197  cphdi  25198  cph2di  25199  cphsubdir  25200  cphsubdi  25201  cph2subdi  25202  cphass  25203  cphassr  25204  ipcau  25230  nmparlem  25231  ipcn  25238  cphsscph  25243  hlphl  25357  cmscsscms  25365  bncssbn  25366  pjthlem2  25430