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=LHypK
dvhlvec.u U=DVecHKW
dvhlvec.k φKHLWH
Assertion dvhlvec φULVec

Proof

Step Hyp Ref Expression
1 dvhlvec.h H=LHypK
2 dvhlvec.u U=DVecHKW
3 dvhlvec.k φKHLWH
4 eqid BaseK=BaseK
5 eqid LTrnKW=LTrnKW
6 eqid TEndoKW=TEndoKW
7 eqid ScalarU=ScalarU
8 eqid +ScalarU=+ScalarU
9 eqid +U=+U
10 eqid 0ScalarU=0ScalarU
11 eqid invgScalarU=invgScalarU
12 eqid ScalarU=ScalarU
13 eqid U=U
14 4 1 5 6 2 7 8 9 10 11 12 13 dvhlveclem KHLWHULVec
15 3 14 syl φULVec