Theorem cphphl 24921

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   ∩ cin 3948   ⊆ wss 3949   ↦ cmpt 5232   “ cima 5680  ‘cfv 6544  (class class class)co 7413  0cc0 11114  +∞cpnf 11251  [,)cico 13332  √csqrt 15186  Basecbs 17150   ↾_s cress 17179  Scalarcsca 17206  ·_𝑖cip 17208  ℂ_fldccnfld 21146  PreHilcphl 21398  normcnm 24307  NrmModcnlm 24311  ℂPreHilccph 24916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-rab 3431  df-v 3474  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-xp 5683  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fv 6552  df-ov 7416  df-cph 24918

This theorem is referenced by:  cphlvec  24925  cphcjcl  24933  cphipcl  24941  cphnmf  24945  cphipcj  24949  cphorthcom  24951  cphip0l  24952  cphip0r  24953  cphipeq0  24954  cphdir  24955  cphdi  24956  cph2di  24957  cphsubdir  24958  cphsubdi  24959  cph2subdi  24960  cphass  24961  cphassr  24962  ipcau  24988  nmparlem  24989  ipcn  24996  cphsscph  25001  hlphl  25115  cmscsscms  25123  bncssbn  25124  pjthlem2  25188