Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cph Structured version   Visualization version   GIF version

Definition df-cph 23874
 Description: Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a subfield of ℂfld closed under square roots of nonnegative reals, we have enough structure to define a norm, with the associated connection to a metric and topology. (Contributed by Mario Carneiro, 8-Oct-2015.)
Assertion
Ref Expression
df-cph ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
Distinct variable group:   𝑓,𝑘,𝑤,𝑥

Detailed syntax breakdown of Definition df-cph
StepHypRef Expression
1 ccph 23872 . 2 class ℂPreHil
2 vf . . . . . . . 8 setvar 𝑓
32cv 1537 . . . . . . 7 class 𝑓
4 ccnfld 20171 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1537 . . . . . . . 8 class 𝑘
7 cress 16547 . . . . . . . 8 class s
84, 6, 7co 7155 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1538 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csqrt 14645 . . . . . . . 8 class
11 cc0 10580 . . . . . . . . . 10 class 0
12 cpnf 10715 . . . . . . . . . 10 class +∞
13 cico 12786 . . . . . . . . . 10 class [,)
1411, 12, 13co 7155 . . . . . . . . 9 class (0[,)+∞)
156, 14cin 3859 . . . . . . . 8 class (𝑘 ∩ (0[,)+∞))
1610, 15cima 5530 . . . . . . 7 class (√ “ (𝑘 ∩ (0[,)+∞)))
1716, 6wss 3860 . . . . . 6 wff (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘
18 vw . . . . . . . . 9 setvar 𝑤
1918cv 1537 . . . . . . . 8 class 𝑤
20 cnm 23283 . . . . . . . 8 class norm
2119, 20cfv 6339 . . . . . . 7 class (norm‘𝑤)
22 vx . . . . . . . 8 setvar 𝑥
23 cbs 16546 . . . . . . . . 9 class Base
2419, 23cfv 6339 . . . . . . . 8 class (Base‘𝑤)
2522cv 1537 . . . . . . . . . 10 class 𝑥
26 cip 16633 . . . . . . . . . . 11 class ·𝑖
2719, 26cfv 6339 . . . . . . . . . 10 class (·𝑖𝑤)
2825, 25, 27co 7155 . . . . . . . . 9 class (𝑥(·𝑖𝑤)𝑥)
2928, 10cfv 6339 . . . . . . . 8 class (√‘(𝑥(·𝑖𝑤)𝑥))
3022, 24, 29cmpt 5115 . . . . . . 7 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
3121, 30wceq 1538 . . . . . 6 wff (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
329, 17, 31w3a 1084 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
333, 23cfv 6339 . . . . 5 class (Base‘𝑓)
3432, 5, 33wsbc 3698 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
35 csca 16631 . . . . 5 class Scalar
3619, 35cfv 6339 . . . 4 class (Scalar‘𝑤)
3734, 2, 36wsbc 3698 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
38 cphl 20394 . . . 4 class PreHil
39 cnlm 23287 . . . 4 class NrmMod
4038, 39cin 3859 . . 3 class (PreHil ∩ NrmMod)
4137, 18, 40crab 3074 . 2 class {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
421, 41wceq 1538 1 wff ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
 Colors of variables: wff setvar class This definition is referenced by:  iscph  23876
 Copyright terms: Public domain W3C validator