Metamath Proof Explorer

Theorem lnmlmod

Description: A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014)

Ref Expression
Assertion lnmlmod 
|- ( M e. LNoeM -> M e. LMod )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
2 1 islnm 
 |-  ( M e. LNoeM <-> ( M e. LMod /\ A. a e. ( LSubSp ` M ) ( M |`s a ) e. LFinGen ) )
3 2 simplbi 
 |-  ( M e. LNoeM -> M e. LMod )