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

Definition df-cph 23014
 Description: Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a quadratically closed subfield of ℂfld, 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 23012 . 2 class ℂPreHil
2 vf . . . . . . . 8 setvar 𝑓
32cv 1522 . . . . . . 7 class 𝑓
4 ccnfld 19794 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1522 . . . . . . . 8 class 𝑘
7 cress 15905 . . . . . . . 8 class s
84, 6, 7co 6690 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1523 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csqrt 14017 . . . . . . . 8 class
11 cc0 9974 . . . . . . . . . 10 class 0
12 cpnf 10109 . . . . . . . . . 10 class +∞
13 cico 12215 . . . . . . . . . 10 class [,)
1411, 12, 13co 6690 . . . . . . . . 9 class (0[,)+∞)
156, 14cin 3606 . . . . . . . 8 class (𝑘 ∩ (0[,)+∞))
1610, 15cima 5146 . . . . . . 7 class (√ “ (𝑘 ∩ (0[,)+∞)))
1716, 6wss 3607 . . . . . 6 wff (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘
18 vw . . . . . . . . 9 setvar 𝑤
1918cv 1522 . . . . . . . 8 class 𝑤
20 cnm 22428 . . . . . . . 8 class norm
2119, 20cfv 5926 . . . . . . 7 class (norm‘𝑤)
22 vx . . . . . . . 8 setvar 𝑥
23 cbs 15904 . . . . . . . . 9 class Base
2419, 23cfv 5926 . . . . . . . 8 class (Base‘𝑤)
2522cv 1522 . . . . . . . . . 10 class 𝑥
26 cip 15993 . . . . . . . . . . 11 class ·𝑖
2719, 26cfv 5926 . . . . . . . . . 10 class (·𝑖𝑤)
2825, 25, 27co 6690 . . . . . . . . 9 class (𝑥(·𝑖𝑤)𝑥)
2928, 10cfv 5926 . . . . . . . 8 class (√‘(𝑥(·𝑖𝑤)𝑥))
3022, 24, 29cmpt 4762 . . . . . . 7 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
3121, 30wceq 1523 . . . . . 6 wff (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
329, 17, 31w3a 1054 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
333, 23cfv 5926 . . . . 5 class (Base‘𝑓)
3432, 5, 33wsbc 3468 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
35 csca 15991 . . . . 5 class Scalar
3619, 35cfv 5926 . . . 4 class (Scalar‘𝑤)
3734, 2, 36wsbc 3468 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
38 cphl 20017 . . . 4 class PreHil
39 cnlm 22432 . . . 4 class NrmMod
4038, 39cin 3606 . . 3 class (PreHil ∩ NrmMod)
4137, 18, 40crab 2945 . 2 class {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
421, 41wceq 1523 1 wff ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
 Colors of variables: wff setvar class This definition is referenced by:  iscph  23016
 Copyright terms: Public domain W3C validator