Theorem lnmlmod

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

	Ref	Expression
Assertion	lnmlmod	⊢ ( 𝑀 ∈ LNoeM → 𝑀 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
2	1	islnm	⊢ ( 𝑀 ∈ LNoeM ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑎 ∈ ( LSubSp ‘ 𝑀 ) ( 𝑀 ↾s 𝑎 ) ∈ LFinGen ) )
3	2	simplbi	⊢ ( 𝑀 ∈ LNoeM → 𝑀 ∈ LMod )