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 = ( LDual ` W )
	lduallmod.w	|- ( ph -> W e. LMod )
Assertion	lduallmod	|- ( ph -> D e. LMod )

Proof

Step	Hyp	Ref	Expression
1		lduallmod.d	|- D = ( LDual ` W )
2		lduallmod.w	|- ( ph -> W e. LMod )
3		eqid	|- ( Base ` W ) = ( Base ` W )
4		eqid	|- oF ( +g ` W ) = oF ( +g ` W )
5		eqid	|- ( LFnl ` W ) = ( LFnl ` W )
6		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
7		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
8		eqid	|- ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
9		eqid	|- ( oppR ` ( Scalar ` W ) ) = ( oppR ` ( Scalar ` W ) )
10		eqid	|- ( .s ` D ) = ( .s ` D )
11	1 2 3 4 5 6 7 8 9 10	lduallmodlem	|- ( ph -> D e. LMod )