Theorem cphphl 23777

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ∩ cin 3937   ⊆ wss 3938   ↦ cmpt 5148   “ cima 5560  ‘cfv 6357  (class class class)co 7158  0cc0 10539  +∞cpnf 10674  [,)cico 12743  √csqrt 14594  Basecbs 16485   ↾_s cress 16486  Scalarcsca 16570  ·_𝑖cip 16572  ℂ_fldccnfld 20547  PreHilcphl 20770  normcnm 23188  NrmModcnlm 23192  ℂPreHilccph 23772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fv 6365  df-ov 7161  df-cph 23774

This theorem is referenced by:  cphlvec  23781  cphcjcl  23789  cphipcl  23797  cphnmf  23801  cphipcj  23805  cphorthcom  23807  cphip0l  23808  cphip0r  23809  cphipeq0  23810  cphdir  23811  cphdi  23812  cph2di  23813  cphsubdir  23814  cphsubdi  23815  cph2subdi  23816  cphass  23817  cphassr  23818  ipcau  23843  nmparlem  23844  ipcn  23851  cphsscph  23856  hlphl  23970  cmscsscms  23978  bncssbn  23979  pjthlem2  24043