Theorem lnmlmod

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

	Ref	Expression
Assertion	lnmlmod	$$⊢M\in \mathrm{LNoeM}\to M\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{LSubSp}\left(M\right)=\mathrm{LSubSp}\left(M\right)$$
2	1	islnm	$$⊢M\in \mathrm{LNoeM}\leftrightarrow \left(M\in \mathrm{LMod}\wedge \forall a\in \mathrm{LSubSp}\left(M\right)M{\upharpoonright }_{𝑠}a\in \mathrm{LFinGen}\right)$$
3	2	simplbi	$$⊢M\in \mathrm{LNoeM}\to M\in \mathrm{LMod}$$