Theorem lduallmod

Description: The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014)

	Ref	Expression
Hypotheses	lduallmod.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	lduallmod.w	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		lduallmod.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
2		lduallmod.w	$$⊢\phi \to W\in \mathrm{LMod}$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4		eqid	$$⊢{\circ }_f{+}_W={\circ }_f{+}_W$$
5		eqid	$$⊢\mathrm{LFnl}\left(W\right)=\mathrm{LFnl}\left(W\right)$$
6		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
8		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(W\right)}={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
9		eqid	$$⊢{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)={opp}_r\left(\mathrm{Scalar}\left(W\right)\right)$$
10		eqid	$$⊢{\cdot }_D={\cdot }_D$$
11	1 2 3 4 5 6 7 8 9 10	lduallmodlem	$$⊢\phi \to D\in \mathrm{LMod}$$