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