![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cphphl | Structured version Visualization version GIF version |
Description: A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
Ref | Expression |
---|---|
cphphl | ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2735 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2735 | . . . 4 ⊢ (·𝑖‘𝑊) = (·𝑖‘𝑊) | |
3 | eqid 2735 | . . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊) | |
4 | eqid 2735 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
5 | eqid 2735 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
6 | 1, 2, 3, 4, 5 | iscph 25218 | . . 3 ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊)))) ∧ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ∧ (norm‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (√‘(𝑥(·𝑖‘𝑊)𝑥))))) |
7 | 6 | simp1bi 1144 | . 2 ⊢ (𝑊 ∈ ℂPreHil → (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊))))) |
8 | 7 | simp1d 1141 | 1 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ∩ cin 3962 ⊆ wss 3963 ↦ cmpt 5231 “ cima 5692 ‘cfv 6563 (class class class)co 7431 0cc0 11153 +∞cpnf 11290 [,)cico 13386 √csqrt 15269 Basecbs 17245 ↾s cress 17274 Scalarcsca 17301 ·𝑖cip 17303 ℂfldccnfld 21382 PreHilcphl 21660 normcnm 24605 NrmModcnlm 24609 ℂPreHilccph 25214 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-nul 5312 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-rab 3434 df-v 3480 df-sbc 3792 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-br 5149 df-opab 5211 df-mpt 5232 df-xp 5695 df-cnv 5697 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-iota 6516 df-fv 6571 df-ov 7434 df-cph 25216 |
This theorem is referenced by: cphlvec 25223 cphcjcl 25231 cphipcl 25239 cphnmf 25243 cphipcj 25247 cphorthcom 25249 cphip0l 25250 cphip0r 25251 cphipeq0 25252 cphdir 25253 cphdi 25254 cph2di 25255 cphsubdir 25256 cphsubdi 25257 cph2subdi 25258 cphass 25259 cphassr 25260 ipcau 25286 nmparlem 25287 ipcn 25294 cphsscph 25299 hlphl 25413 cmscsscms 25421 bncssbn 25422 pjthlem2 25486 |
Copyright terms: Public domain | W3C validator |