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 = ( Scalar ` M )
	lnrfgtr.u	|- U = ( LSubSp ` M )
	lnrfgtr.n	|- N = ( M |`s P )
Assertion	lnrfgtr	|- ( ( M e. LFinGen /\ S e. LNoeR /\ P e. U ) -> N e. LFinGen )

Proof

Step	Hyp	Ref	Expression
1		lnrfg.s	|- S = ( Scalar ` M )
2		lnrfgtr.u	|- U = ( LSubSp ` M )
3		lnrfgtr.n	|- N = ( M |`s P )
4	1	lnrfg	|- ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM )
5	2 3	lnmlssfg	|- ( ( M e. LNoeM /\ P e. U ) -> N e. LFinGen )
6	4 5	stoic3	|- ( ( M e. LFinGen /\ S e. LNoeR /\ P e. U ) -> N e. LFinGen )