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

Definition df-cph 18620
Description: Define a complex pre-Hilbert space. By restricting the scalar field to a quadratically closed subfield of  CC, 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  |-  CPreHil  =  {
w  e.  ( PreHil  i^i NrmMod )  |  [. (Scalar `  w )  /  f ]. [. ( Base `  f
)  /  k ]. ( f  =  (flds  k )  /\  ( sqr " (
k  i^i  ( 0 [,)  +oo ) ) ) 
C_  k  /\  ( norm `  w )  =  ( x  e.  (
Base `  w )  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) ) }
Distinct variable group:    f, k, w, x

Detailed syntax breakdown of Definition df-cph
StepHypRef Expression
1 ccph 18618 . 2  class  CPreHil
2 vf . . . . . . . 8  set  f
32cv 1631 . . . . . . 7  class  f
4 ccnfld 16393 . . . . . . . 8  classfld
5 vk . . . . . . . . 9  set  k
65cv 1631 . . . . . . . 8  class  k
7 cress 13165 . . . . . . . 8  classs
84, 6, 7co 5874 . . . . . . 7  class  (flds  k )
93, 8wceq 1632 . . . . . 6  wff  f  =  (flds  k )
10 csqr 11734 . . . . . . . 8  class  sqr
11 cc0 8753 . . . . . . . . . 10  class  0
12 cpnf 8880 . . . . . . . . . 10  class  +oo
13 cico 10674 . . . . . . . . . 10  class  [,)
1411, 12, 13co 5874 . . . . . . . . 9  class  ( 0 [,)  +oo )
156, 14cin 3164 . . . . . . . 8  class  ( k  i^i  ( 0 [,) 
+oo ) )
1610, 15cima 4708 . . . . . . 7  class  ( sqr " ( k  i^i  ( 0 [,)  +oo ) ) )
1716, 6wss 3165 . . . . . 6  wff  ( sqr " ( k  i^i  ( 0 [,)  +oo ) ) )  C_  k
18 vw . . . . . . . . 9  set  w
1918cv 1631 . . . . . . . 8  class  w
20 cnm 18115 . . . . . . . 8  class  norm
2119, 20cfv 5271 . . . . . . 7  class  ( norm `  w )
22 vx . . . . . . . 8  set  x
23 cbs 13164 . . . . . . . . 9  class  Base
2419, 23cfv 5271 . . . . . . . 8  class  ( Base `  w )
2522cv 1631 . . . . . . . . . 10  class  x
26 cip 13229 . . . . . . . . . . 11  class  .i
2719, 26cfv 5271 . . . . . . . . . 10  class  ( .i
`  w )
2825, 25, 27co 5874 . . . . . . . . 9  class  ( x ( .i `  w
) x )
2928, 10cfv 5271 . . . . . . . 8  class  ( sqr `  ( x ( .i
`  w ) x ) )
3022, 24, 29cmpt 4093 . . . . . . 7  class  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) )
3121, 30wceq 1632 . . . . . 6  wff  ( norm `  w )  =  ( x  e.  ( Base `  w )  |->  ( sqr `  ( x ( .i
`  w ) x ) ) )
329, 17, 31w3a 934 . . . . 5  wff  ( f  =  (flds  k )  /\  ( sqr " ( k  i^i  ( 0 [,)  +oo ) ) )  C_  k  /\  ( norm `  w
)  =  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) )
333, 23cfv 5271 . . . . 5  class  ( Base `  f )
3432, 5, 33wsbc 3004 . . . 4  wff  [. ( Base `  f )  / 
k ]. ( f  =  (flds  k )  /\  ( sqr " ( k  i^i  ( 0 [,)  +oo ) ) )  C_  k  /\  ( norm `  w
)  =  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) )
35 csca 13227 . . . . 5  class Scalar
3619, 35cfv 5271 . . . 4  class  (Scalar `  w )
3734, 2, 36wsbc 3004 . . 3  wff  [. (Scalar `  w )  /  f ]. [. ( Base `  f
)  /  k ]. ( f  =  (flds  k )  /\  ( sqr " (
k  i^i  ( 0 [,)  +oo ) ) ) 
C_  k  /\  ( norm `  w )  =  ( x  e.  (
Base `  w )  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) )
38 cphl 16544 . . . 4  class  PreHil
39 cnlm 18119 . . . 4  class NrmMod
4038, 39cin 3164 . . 3  class  ( PreHil  i^i NrmMod )
4137, 18, 40crab 2560 . 2  class  { w  e.  ( PreHil  i^i NrmMod )  |  [. (Scalar `  w )  / 
f ]. [. ( Base `  f )  /  k ]. ( f  =  (flds  k )  /\  ( sqr " (
k  i^i  ( 0 [,)  +oo ) ) ) 
C_  k  /\  ( norm `  w )  =  ( x  e.  (
Base `  w )  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) ) }
421, 41wceq 1632 1  wff  CPreHil  =  {
w  e.  ( PreHil  i^i NrmMod )  |  [. (Scalar `  w )  /  f ]. [. ( Base `  f
)  /  k ]. ( f  =  (flds  k )  /\  ( sqr " (
k  i^i  ( 0 [,)  +oo ) ) ) 
C_  k  /\  ( norm `  w )  =  ( x  e.  (
Base `  w )  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  iscph  18622
  Copyright terms: Public domain W3C validator