# 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}=\mathrm{LSubSp}\left({M}\right)$
lnmlssfg.r ${⊢}{R}={M}{↾}_{𝑠}{U}$
Assertion lnmlssfg ${⊢}\left({M}\in \mathrm{LNoeM}\wedge {U}\in {S}\right)\to {R}\in \mathrm{LFinGen}$

### Proof

Step Hyp Ref Expression
1 lnmlssfg.s ${⊢}{S}=\mathrm{LSubSp}\left({M}\right)$
2 lnmlssfg.r ${⊢}{R}={M}{↾}_{𝑠}{U}$
3 1 islnm ${⊢}{M}\in \mathrm{LNoeM}↔\left({M}\in \mathrm{LMod}\wedge \forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{M}{↾}_{𝑠}{a}\in \mathrm{LFinGen}\right)$
4 3 simprbi ${⊢}{M}\in \mathrm{LNoeM}\to \forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{M}{↾}_{𝑠}{a}\in \mathrm{LFinGen}$
5 oveq2 ${⊢}{a}={U}\to {M}{↾}_{𝑠}{a}={M}{↾}_{𝑠}{U}$
6 5 2 eqtr4di ${⊢}{a}={U}\to {M}{↾}_{𝑠}{a}={R}$
7 6 eleq1d ${⊢}{a}={U}\to \left({M}{↾}_{𝑠}{a}\in \mathrm{LFinGen}↔{R}\in \mathrm{LFinGen}\right)$
8 7 rspcv ${⊢}{U}\in {S}\to \left(\forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{M}{↾}_{𝑠}{a}\in \mathrm{LFinGen}\to {R}\in \mathrm{LFinGen}\right)$
9 4 8 mpan9 ${⊢}\left({M}\in \mathrm{LNoeM}\wedge {U}\in {S}\right)\to {R}\in \mathrm{LFinGen}$