Description: The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hlhilslem.h | |- H = ( LHyp ` K ) |
|
| hlhilslem.e | |- E = ( ( EDRing ` K ) ` W ) |
||
| hlhilslem.u | |- U = ( ( HLHil ` K ) ` W ) |
||
| hlhilslem.r | |- R = ( Scalar ` U ) |
||
| hlhilslem.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| hlhilsbase.c | |- C = ( Base ` E ) |
||
| Assertion | hlhilsbase | |- ( ph -> C = ( Base ` R ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlhilslem.h | |- H = ( LHyp ` K ) |
|
| 2 | hlhilslem.e | |- E = ( ( EDRing ` K ) ` W ) |
|
| 3 | hlhilslem.u | |- U = ( ( HLHil ` K ) ` W ) |
|
| 4 | hlhilslem.r | |- R = ( Scalar ` U ) |
|
| 5 | hlhilslem.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 6 | hlhilsbase.c | |- C = ( Base ` E ) |
|
| 7 | df-base | |- Base = Slot 1 |
|
| 8 | 1nn | |- 1 e. NN |
|
| 9 | 1lt4 | |- 1 < 4 |
|
| 10 | 1 2 3 4 5 7 8 9 6 | hlhilslem | |- ( ph -> C = ( Base ` R ) ) |