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	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	lduallmod.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		lduallmod.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
2		lduallmod.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
3		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4		eqid	⊢ ∘f ( +g ‘ 𝑊 ) = ∘f ( +g ‘ 𝑊 )
5		eqid	⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
6		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
8		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
9		eqid	⊢ ( oppr ‘ ( Scalar ‘ 𝑊 ) ) = ( oppr ‘ ( Scalar ‘ 𝑊 ) )
10		eqid	⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
11	1 2 3 4 5 6 7 8 9 10	lduallmodlem	⊢ ( 𝜑 → 𝐷 ∈ LMod )