![]() |
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 2736 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2736 | . . . 4 ⊢ (·𝑖‘𝑊) = (·𝑖‘𝑊) | |
3 | eqid 2736 | . . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊) | |
4 | eqid 2736 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
5 | eqid 2736 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
6 | 1, 2, 3, 4, 5 | iscph 24518 | . . 3 ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊)))) ∧ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ∧ (norm‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (√‘(𝑥(·𝑖‘𝑊)𝑥))))) |
7 | 6 | simp1bi 1145 | . 2 ⊢ (𝑊 ∈ ℂPreHil → (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊))))) |
8 | 7 | simp1d 1142 | 1 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∩ cin 3907 ⊆ wss 3908 ↦ cmpt 5186 “ cima 5634 ‘cfv 6493 (class class class)co 7353 0cc0 11047 +∞cpnf 11182 [,)cico 13258 √csqrt 15110 Basecbs 17075 ↾s cress 17104 Scalarcsca 17128 ·𝑖cip 17130 ℂfldccnfld 20781 PreHilcphl 21013 normcnm 23916 NrmModcnlm 23920 ℂPreHilccph 24514 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-nul 5261 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2942 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-xp 5637 df-cnv 5639 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6445 df-fv 6501 df-ov 7356 df-cph 24516 |
This theorem is referenced by: cphlvec 24523 cphcjcl 24531 cphipcl 24539 cphnmf 24543 cphipcj 24547 cphorthcom 24549 cphip0l 24550 cphip0r 24551 cphipeq0 24552 cphdir 24553 cphdi 24554 cph2di 24555 cphsubdir 24556 cphsubdi 24557 cph2subdi 24558 cphass 24559 cphassr 24560 ipcau 24586 nmparlem 24587 ipcn 24594 cphsscph 24599 hlphl 24713 cmscsscms 24721 bncssbn 24722 pjthlem2 24786 |
Copyright terms: Public domain | W3C validator |