Description: A subcomplex pre-Hilbert space is a vector space over a subfield of CCfld . (Contributed by Mario Carneiro, 8-Oct-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cphsca.f | |- F = ( Scalar ` W ) |
|
| cphsca.k | |- K = ( Base ` F ) |
||
| Assertion | cphsca | |- ( W e. CPreHil -> F = ( CCfld |`s K ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cphsca.f | |- F = ( Scalar ` W ) |
|
| 2 | cphsca.k | |- K = ( Base ` F ) |
|
| 3 | eqid | |- ( Base ` W ) = ( Base ` W ) |
|
| 4 | eqid | |- ( .i ` W ) = ( .i ` W ) |
|
| 5 | eqid | |- ( norm ` W ) = ( norm ` W ) |
|
| 6 | 3 4 5 1 2 | iscph | |- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ ( norm ` W ) = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) ) ) |
| 7 | 6 | simp1bi | |- ( W e. CPreHil -> ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) ) |
| 8 | 7 | simp3d | |- ( W e. CPreHil -> F = ( CCfld |`s K ) ) |