Metamath Proof Explorer


Theorem lnrfgtr

Description: A submodule of a finitely generated module over a Noetherian ring is finitely generated. Often taken as the definition of Noetherian ring. (Contributed by Stefan O'Rear, 7-Feb-2015)

Ref Expression
Hypotheses lnrfg.s S=ScalarM
lnrfgtr.u U=LSubSpM
lnrfgtr.n N=M𝑠P
Assertion lnrfgtr MLFinGenSLNoeRPUNLFinGen

Proof

Step Hyp Ref Expression
1 lnrfg.s S=ScalarM
2 lnrfgtr.u U=LSubSpM
3 lnrfgtr.n N=M𝑠P
4 1 lnrfg MLFinGenSLNoeRMLNoeM
5 2 3 lnmlssfg MLNoeMPUNLFinGen
6 4 5 stoic3 MLFinGenSLNoeRPUNLFinGen