![]() |
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 2778 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2778 | . . . 4 ⊢ (·𝑖‘𝑊) = (·𝑖‘𝑊) | |
3 | eqid 2778 | . . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊) | |
4 | eqid 2778 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
5 | eqid 2778 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
6 | 1, 2, 3, 4, 5 | iscph 23377 | . . 3 ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊)))) ∧ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ∧ (norm‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (√‘(𝑥(·𝑖‘𝑊)𝑥))))) |
7 | 6 | simp1bi 1136 | . 2 ⊢ (𝑊 ∈ ℂPreHil → (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊))))) |
8 | 7 | simp1d 1133 | 1 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 = wceq 1601 ∈ wcel 2107 ∩ cin 3791 ⊆ wss 3792 ↦ cmpt 4965 “ cima 5358 ‘cfv 6135 (class class class)co 6922 0cc0 10272 +∞cpnf 10408 [,)cico 12489 √csqrt 14380 Basecbs 16255 ↾s cress 16256 Scalarcsca 16341 ·𝑖cip 16343 ℂfldccnfld 20142 PreHilcphl 20367 normcnm 22789 NrmModcnlm 22793 ℂPreHilccph 23373 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-nul 5025 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-mpt 4966 df-xp 5361 df-cnv 5363 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-iota 6099 df-fv 6143 df-ov 6925 df-cph 23375 |
This theorem is referenced by: cphlvec 23382 cphcjcl 23390 cphipcl 23398 cphnmf 23402 cphipcj 23406 cphorthcom 23408 cphip0l 23409 cphip0r 23410 cphipeq0 23411 cphdir 23412 cphdi 23413 cph2di 23414 cphsubdir 23415 cphsubdi 23416 cph2subdi 23417 cphass 23418 cphassr 23419 ipcau 23444 nmparlem 23445 ipcn 23452 cphsscph 23457 hlphl 23571 cmscsscms 23579 bncssbn 23580 pjthlem2 23644 |
Copyright terms: Public domain | W3C validator |