Metamath Proof Explorer

Definition df-cph

Description: Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a subfield of CCfld 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)

Ref Expression
Assertion df-cph 
|- CPreHil = { w e. ( PreHil i^i NrmMod ) | [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccph 
 |-  CPreHil
1 vw 
 |-  w
2 cphl 
 |-  PreHil
3 cnlm 
 |-  NrmMod
4 2 3 cin 
 |-  ( PreHil i^i NrmMod )
5 csca 
 |-  Scalar
6 1 cv 
 |-  w
7 6 5 cfv 
 |-  ( Scalar ` w )
8 vf 
 |-  f
9 cbs 
 |-  Base
10 8 cv 
 |-  f
11 10 9 cfv 
 |-  ( Base ` f )
12 vk 
 |-  k
13 ccnfld 
 |-  CCfld
14 cress 
 |-  |`s
15 12 cv 
 |-  k
16 13 15 14 co 
 |-  ( CCfld |`s k )
17 10 16 wceq 
 |-  f = ( CCfld |`s k )
18 csqrt 
 |-  sqrt
19 cc0 
 |-  0
20 cico 
 |-  [,)
21 cpnf 
 |-  +oo
22 19 21 20 co 
 |-  ( 0 [,) +oo )
23 15 22 cin 
 |-  ( k i^i ( 0 [,) +oo ) )
24 18 23 cima 
 |-  ( sqrt " ( k i^i ( 0 [,) +oo ) ) )
25 24 15 wss 
 |-  ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k
26 cnm 
 |-  norm
27 6 26 cfv 
 |-  ( norm ` w )
28 vx 
 |-  x
29 6 9 cfv 
 |-  ( Base ` w )
30 28 cv 
 |-  x
31 cip 
 |-  .i
32 6 31 cfv 
 |-  ( .i ` w )
33 30 30 32 co 
 |-  ( x ( .i ` w ) x )
34 33 18 cfv 
 |-  ( sqrt ` ( x ( .i ` w ) x ) )
35 28 29 34 cmpt 
 |-  ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) )
36 27 35 wceq 
 |-  ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) )
37 17 25 36 w3a 
 |-  ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) )
38 37 12 11 wsbc 
 |-  [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) )
39 38 8 7 wsbc 
 |-  [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) )
40 39 1 4 crab 
 |-  { w e. ( PreHil i^i NrmMod ) | [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) }
41 0 40 wceq 
 |-  CPreHil = { w e. ( PreHil i^i NrmMod ) | [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) }