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

Definition df-cph 23295
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 23293 . 2 class ℂPreHil
2 vf . . . . . . . 8 setvar 𝑓
32cv 1652 . . . . . . 7 class 𝑓
4 ccnfld 20068 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1652 . . . . . . . 8 class 𝑘
7 cress 16185 . . . . . . . 8 class s
84, 6, 7co 6878 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1653 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csqrt 14314 . . . . . . . 8 class
11 cc0 10224 . . . . . . . . . 10 class 0
12 cpnf 10360 . . . . . . . . . 10 class +∞
13 cico 12426 . . . . . . . . . 10 class [,)
1411, 12, 13co 6878 . . . . . . . . 9 class (0[,)+∞)
156, 14cin 3768 . . . . . . . 8 class (𝑘 ∩ (0[,)+∞))
1610, 15cima 5315 . . . . . . 7 class (√ “ (𝑘 ∩ (0[,)+∞)))
1716, 6wss 3769 . . . . . 6 wff (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘
18 vw . . . . . . . . 9 setvar 𝑤
1918cv 1652 . . . . . . . 8 class 𝑤
20 cnm 22709 . . . . . . . 8 class norm
2119, 20cfv 6101 . . . . . . 7 class (norm‘𝑤)
22 vx . . . . . . . 8 setvar 𝑥
23 cbs 16184 . . . . . . . . 9 class Base
2419, 23cfv 6101 . . . . . . . 8 class (Base‘𝑤)
2522cv 1652 . . . . . . . . . 10 class 𝑥
26 cip 16272 . . . . . . . . . . 11 class ·𝑖
2719, 26cfv 6101 . . . . . . . . . 10 class (·𝑖𝑤)
2825, 25, 27co 6878 . . . . . . . . 9 class (𝑥(·𝑖𝑤)𝑥)
2928, 10cfv 6101 . . . . . . . 8 class (√‘(𝑥(·𝑖𝑤)𝑥))
3022, 24, 29cmpt 4922 . . . . . . 7 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
3121, 30wceq 1653 . . . . . 6 wff (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
329, 17, 31w3a 1108 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
333, 23cfv 6101 . . . . 5 class (Base‘𝑓)
3432, 5, 33wsbc 3633 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
35 csca 16270 . . . . 5 class Scalar
3619, 35cfv 6101 . . . 4 class (Scalar‘𝑤)
3734, 2, 36wsbc 3633 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
38 cphl 20293 . . . 4 class PreHil
39 cnlm 22713 . . . 4 class NrmMod
4038, 39cin 3768 . . 3 class (PreHil ∩ NrmMod)
4137, 18, 40crab 3093 . 2 class {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
421, 41wceq 1653 1 wff ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
Colors of variables: wff setvar class
This definition is referenced by:  iscph  23297
  Copyright terms: Public domain W3C validator