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}$$