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 e. LNoeM -> M e. LFinGen )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` M ) = ( Base ` M )
2 1 ressid 
 |-  ( M e. LNoeM -> ( M |`s ( Base ` M ) ) = M )
3 lnmlmod 
 |-  ( M e. LNoeM -> M e. LMod )
4 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
5 1 4 lss1 
 |-  ( M e. LMod -> ( Base ` M ) e. ( LSubSp ` M ) )
6 3 5 syl 
 |-  ( M e. LNoeM -> ( Base ` M ) e. ( LSubSp ` M ) )
7 eqid 
 |-  ( M |`s ( Base ` M ) ) = ( M |`s ( Base ` M ) )
8 4 7 lnmlssfg 
 |-  ( ( M e. LNoeM /\ ( Base ` M ) e. ( LSubSp ` M ) ) -> ( M |`s ( Base ` M ) ) e. LFinGen )
9 6 8 mpdan 
 |-  ( M e. LNoeM -> ( M |`s ( Base ` M ) ) e. LFinGen )
10 2 9 eqeltrrd 
 |-  ( M e. LNoeM -> M e. LFinGen )