Theorem dvalvec

Description: The constructed partial vector space A for a lattice K is a left vector space. (Contributed by NM, 11-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dvalvec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvalvec.v	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
Assertion	dvalvec	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to U\in \mathrm{LVec}$$

Proof

Step	Hyp	Ref	Expression
1		dvalvec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvalvec.v	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
3		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		eqid	$$⊢{+}_U={+}_U$$
5		eqid	$$⊢\mathrm{TEndo}\left(K\right)\left(W\right)=\mathrm{TEndo}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
7		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
8		eqid	$$⊢{+}_{\mathrm{Scalar}\left(U\right)}={+}_{\mathrm{Scalar}\left(U\right)}$$
9		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(U\right)}={\cdot }_{\mathrm{Scalar}\left(U\right)}$$
10		eqid	$$⊢{\cdot }_U={\cdot }_U$$
11	1 2 3 4 5 6 7 8 9 10	dvalveclem	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to U\in \mathrm{LVec}$$