Theorem cphphl 25341

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142   ∩ cin 3903   ⊆ wss 3904   ↦ cmpt 5191   “ cima 5663  ‘cfv 6536  (class class class)co 7412  0cc0 11106  +∞cpnf 11246  [,)cico 13380  √csqrt 15291  Basecbs 17275   ↾_s cress 17296  Scalarcsca 17319  ·_𝑖cip 17321  ℂ_fldccnfld 21533  PreHilcphl 21785  normcnm 24744  NrmModcnlm 24748  ℂPreHilccph 25336

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-xp 5666  df-cnv 5668  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fv 6544  df-ov 7415  df-cph 25338

This theorem is used by:  cphlvec  25345  cphcjcl  25353  cphipcl  25361  cphnmf  25365  cphipcj  25369  cphorthcom  25371  cphip0l  25372  cphip0r  25373  cphipeq0  25374  cphdir  25375  cphdi  25376  cph2di  25377  cphsubdir  25378  cphsubdi  25379  cph2subdi  25380  cphass  25381  cphassr  25382  ipcau  25408  nmparlem  25409  ipcn  25416  cphsscph  25421  hlphl  25535  cmscsscms  25543  bncssbn  25544  pjthlem2  25608