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 ∈ LNoeM → M ∈ LMod

Proof

Step Hyp Ref Expression
1 eqid ⊢ LSubSp ⁡ M = LSubSp ⁡ M
2 1 islnm ⊢ M ∈ LNoeM ↔ M ∈ LMod ∧ ∀ a ∈ LSubSp ⁡ M M ↾ 𝑠 a ∈ LFinGen
3 2 simplbi ⊢ M ∈ LNoeM → M ∈ LMod