Theorem cphphl 25472

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 2761	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2761	. . . 4 ⊢ (·𝑖‘𝑊) = (·𝑖‘𝑊)
3		eqid 2761	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
4		eqid 2761	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2761	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6	1, 2, 3, 4, 5	iscph 25471	. . 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)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ∩ cin 3898   ⊆ wss 3899   ↦ cmpt 5186   “ cima 5654  ‘cfv 6531  (class class class)co 7412  0cc0 11181  +∞cpnf 11321  [,)cico 13459  √csqrt 15380  Basecbs 17367   ↾_s cress 17388  Scalarcsca 17411  ·_𝑖cip 17413  ℂ_fldccnfld 21658  PreHilcphl 21910  normcnm 24875  NrmModcnlm 24879  ℂPreHilccph 25467

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fv 6539  df-ov 7415  df-cph 25469

This theorem is used by:  cphlvec  25476  cphcjcl  25484  cphipcl  25492  cphnmf  25496  cphipcj  25500  cphorthcom  25502  cphip0l  25503  cphip0r  25504  cphipeq0  25505  cphdir  25506  cphdi  25507  cph2di  25508  cphsubdir  25509  cphsubdi  25510  cph2subdi  25511  cphass  25512  cphassr  25513  ipcau  25539  nmparlem  25540  ipcn  25547  cphsscph  25552  hlphl  25666  cmscsscms  25674  bncssbn  25675  pjthlem2  25739