# Metamath Proof Explorer

## Theorem dvhlvec

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 dvhlvec
`|- ( ph -> U e. LVec )`

### Proof

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 eqid
` |-  ( Base ` K ) = ( Base ` K )`
5 eqid
` |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )`
6 eqid
` |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )`
7 eqid
` |-  ( Scalar ` U ) = ( Scalar ` U )`
8 eqid
` |-  ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )`
9 eqid
` |-  ( +g ` U ) = ( +g ` U )`
10 eqid
` |-  ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )`
11 eqid
` |-  ( invg ` ( Scalar ` U ) ) = ( invg ` ( Scalar ` U ) )`
12 eqid
` |-  ( .r ` ( Scalar ` U ) ) = ( .r ` ( Scalar ` U ) )`
13 eqid
` |-  ( .s ` U ) = ( .s ` U )`
14 4 1 5 6 2 7 8 9 10 11 12 13 dvhlveclem
` |-  ( ( K e. HL /\ W e. H ) -> U e. LVec )`
15 3 14 syl
` |-  ( ph -> U e. LVec )`