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 ) |
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 ) |