Theorem cphphl 25311

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ∩ cin 3905   ⊆ wss 3906   ↦ cmpt 5193   “ cima 5666  ‘cfv 6538  (class class class)co 7412  0cc0 11101  +∞cpnf 11241  [,)cico 13375  √csqrt 15286  Basecbs 17270   ↾_s cress 17291  Scalarcsca 17314  ·_𝑖cip 17316  ℂ_fldccnfld 21503  PreHilcphl 21755  normcnm 24714  NrmModcnlm 24718  ℂPreHilccph 25306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fv 6546  df-ov 7415  df-cph 25308

This theorem is referenced by:  cphlvec  25315  cphcjcl  25323  cphipcl  25331  cphnmf  25335  cphipcj  25339  cphorthcom  25341  cphip0l  25342  cphip0r  25343  cphipeq0  25344  cphdir  25345  cphdi  25346  cph2di  25347  cphsubdir  25348  cphsubdi  25349  cph2subdi  25350  cphass  25351  cphassr  25352  ipcau  25378  nmparlem  25379  ipcn  25386  cphsscph  25391  hlphl  25505  cmscsscms  25513  bncssbn  25514  pjthlem2  25578