Description: The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W ) is a left module. (Contributed by NM, 23-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dvhlvec.h | |- H = ( LHyp ` K ) |
|
| dvhlvec.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| dvhlvec.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| Assertion | dvhlmod | |- ( ph -> U e. LMod ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dvhlvec.h | |- H = ( LHyp ` K ) |
|
| 2 | dvhlvec.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 3 | dvhlvec.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 4 | 1 2 3 | dvhlvec | |- ( ph -> U e. LVec ) |
| 5 | lveclmod | |- ( U e. LVec -> U e. LMod ) |
|
| 6 | 4 5 | syl | |- ( ph -> U e. LMod ) |