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 22700
Description: Define a complex pre-Hilbert space. By restricting the scalar field to a quadratically closed subfield of , 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 22698 . 2 class ℂPreHil
2 vf . . . . . . . 8 setvar 𝑓
32cv 1473 . . . . . . 7 class 𝑓
4 ccnfld 19513 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1473 . . . . . . . 8 class 𝑘
7 cress 15642 . . . . . . . 8 class s
84, 6, 7co 6527 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1474 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csqrt 13767 . . . . . . . 8 class
11 cc0 9792 . . . . . . . . . 10 class 0
12 cpnf 9927 . . . . . . . . . 10 class +∞
13 cico 12004 . . . . . . . . . 10 class [,)
1411, 12, 13co 6527 . . . . . . . . 9 class (0[,)+∞)
156, 14cin 3538 . . . . . . . 8 class (𝑘 ∩ (0[,)+∞))
1610, 15cima 5031 . . . . . . 7 class (√ “ (𝑘 ∩ (0[,)+∞)))
1716, 6wss 3539 . . . . . 6 wff (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘
18 vw . . . . . . . . 9 setvar 𝑤
1918cv 1473 . . . . . . . 8 class 𝑤
20 cnm 22132 . . . . . . . 8 class norm
2119, 20cfv 5790 . . . . . . 7 class (norm‘𝑤)
22 vx . . . . . . . 8 setvar 𝑥
23 cbs 15641 . . . . . . . . 9 class Base
2419, 23cfv 5790 . . . . . . . 8 class (Base‘𝑤)
2522cv 1473 . . . . . . . . . 10 class 𝑥
26 cip 15719 . . . . . . . . . . 11 class ·𝑖
2719, 26cfv 5790 . . . . . . . . . 10 class (·𝑖𝑤)
2825, 25, 27co 6527 . . . . . . . . 9 class (𝑥(·𝑖𝑤)𝑥)
2928, 10cfv 5790 . . . . . . . 8 class (√‘(𝑥(·𝑖𝑤)𝑥))
3022, 24, 29cmpt 4637 . . . . . . 7 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
3121, 30wceq 1474 . . . . . 6 wff (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
329, 17, 31w3a 1030 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
333, 23cfv 5790 . . . . 5 class (Base‘𝑓)
3432, 5, 33wsbc 3401 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
35 csca 15717 . . . . 5 class Scalar
3619, 35cfv 5790 . . . 4 class (Scalar‘𝑤)
3734, 2, 36wsbc 3401 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
38 cphl 19733 . . . 4 class PreHil
39 cnlm 22136 . . . 4 class NrmMod
4038, 39cin 3538 . . 3 class (PreHil ∩ NrmMod)
4137, 18, 40crab 2899 . 2 class {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
421, 41wceq 1474 1 wff ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))}
Colors of variables: wff setvar class
This definition is referenced by:  iscph  22702
  Copyright terms: Public domain W3C validator