Metamath Proof Explorer

Theorem lnmfg

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

Ref Expression
Assertion lnmfg ⊢ M ∈ LNoeM → M ∈ LFinGen

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base M = Base M
2 1 ressid ⊢ M ∈ LNoeM → M ↾ 𝑠 Base M = M
3 lnmlmod ⊢ M ∈ LNoeM → M ∈ LMod
4 eqid ⊢ LSubSp ⁡ M = LSubSp ⁡ M
5 1 4 lss1 ⊢ M ∈ LMod → Base M ∈ LSubSp ⁡ M
6 3 5 syl ⊢ M ∈ LNoeM → Base M ∈ LSubSp ⁡ M
7 eqid ⊢ M ↾ 𝑠 Base M = M ↾ 𝑠 Base M
8 4 7 lnmlssfg ⊢ M ∈ LNoeM ∧ Base M ∈ LSubSp ⁡ M → M ↾ 𝑠 Base M ∈ LFinGen
9 6 8 mpdan ⊢ M ∈ LNoeM → M ↾ 𝑠 Base M ∈ LFinGen
10 2 9 eqeltrrd ⊢ M ∈ LNoeM → M ∈ LFinGen