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}=\mathrm{LHyp}\left({K}\right)$
dvhlvec.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvhlvec.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$

Proof

Step Hyp Ref Expression
1 dvhlvec.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dvhlvec.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dvhlvec.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
4 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
5 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 eqid ${⊢}\mathrm{TEndo}\left({K}\right)\left({W}\right)=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
7 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
8 eqid ${⊢}{+}_{\mathrm{Scalar}\left({U}\right)}={+}_{\mathrm{Scalar}\left({U}\right)}$
9 eqid ${⊢}{+}_{{U}}={+}_{{U}}$
10 eqid ${⊢}{0}_{\mathrm{Scalar}\left({U}\right)}={0}_{\mathrm{Scalar}\left({U}\right)}$
11 eqid ${⊢}{inv}_{g}\left(\mathrm{Scalar}\left({U}\right)\right)={inv}_{g}\left(\mathrm{Scalar}\left({U}\right)\right)$
12 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({U}\right)}={\cdot }_{\mathrm{Scalar}\left({U}\right)}$
13 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
14 4 1 5 6 2 7 8 9 10 11 12 13 dvhlveclem ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{LVec}$
15 3 14 syl ${⊢}{\phi }\to {U}\in \mathrm{LVec}$