Metamath Proof Explorer

Theorem clmlmod

Description: A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion clmlmod 
|- ( W e. CMod -> W e. LMod )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
2 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
3 1 2 isclm 
 |-  ( W e. CMod <-> ( W e. LMod /\ ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) /\ ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) ) )
4 3 simp1bi 
 |-  ( W e. CMod -> W e. LMod )