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

Definition df-cph 19131
 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 NrmMod Scalar flds
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-cph
StepHypRef Expression
1 ccph 19129 . 2
2 vf . . . . . . . 8
32cv 1651 . . . . . . 7
4 ccnfld 16703 . . . . . . . 8 fld
5 vk . . . . . . . . 9
65cv 1651 . . . . . . . 8
7 cress 13470 . . . . . . . 8 s
84, 6, 7co 6081 . . . . . . 7 flds
93, 8wceq 1652 . . . . . 6 flds
10 csqr 12038 . . . . . . . 8
11 cc0 8990 . . . . . . . . . 10
12 cpnf 9117 . . . . . . . . . 10
13 cico 10918 . . . . . . . . . 10
1411, 12, 13co 6081 . . . . . . . . 9
156, 14cin 3319 . . . . . . . 8
1610, 15cima 4881 . . . . . . 7
1716, 6wss 3320 . . . . . 6
18 vw . . . . . . . . 9
1918cv 1651 . . . . . . . 8
20 cnm 18624 . . . . . . . 8
2119, 20cfv 5454 . . . . . . 7
22 vx . . . . . . . 8
23 cbs 13469 . . . . . . . . 9
2419, 23cfv 5454 . . . . . . . 8
2522cv 1651 . . . . . . . . . 10
26 cip 13534 . . . . . . . . . . 11
2719, 26cfv 5454 . . . . . . . . . 10
2825, 25, 27co 6081 . . . . . . . . 9
2928, 10cfv 5454 . . . . . . . 8
3022, 24, 29cmpt 4266 . . . . . . 7
3121, 30wceq 1652 . . . . . 6
329, 17, 31w3a 936 . . . . 5 flds
333, 23cfv 5454 . . . . 5
3432, 5, 33wsbc 3161 . . . 4 flds
35 csca 13532 . . . . 5 Scalar
3619, 35cfv 5454 . . . 4 Scalar
3734, 2, 36wsbc 3161 . . 3 Scalar flds
38 cphl 16855 . . . 4
39 cnlm 18628 . . . 4 NrmMod
4038, 39cin 3319 . . 3 NrmMod
4137, 18, 40crab 2709 . 2 NrmMod Scalar flds
421, 41wceq 1652 1 NrmMod Scalar flds
 Colors of variables: wff set class This definition is referenced by:  iscph  19133
 Copyright terms: Public domain W3C validator