This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )