Metamath Proof Explorer


Theorem lnmlssfg

Description: A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lnmlssfg.s S = LSubSp M
lnmlssfg.r R = M 𝑠 U
Assertion lnmlssfg M LNoeM U S R LFinGen

Proof

Step Hyp Ref Expression
1 lnmlssfg.s S = LSubSp M
2 lnmlssfg.r R = M 𝑠 U
3 1 islnm M LNoeM M LMod a S M 𝑠 a LFinGen
4 3 simprbi M LNoeM a S M 𝑠 a LFinGen
5 oveq2 a = U M 𝑠 a = M 𝑠 U
6 5 2 eqtr4di a = U M 𝑠 a = R
7 6 eleq1d a = U M 𝑠 a LFinGen R LFinGen
8 7 rspcv U S a S M 𝑠 a LFinGen R LFinGen
9 4 8 mpan9 M LNoeM U S R LFinGen