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 |`s U )
Assertion	lnmlssfg	|- ( ( M e. LNoeM /\ U e. S ) -> R e. LFinGen )

Proof

Step	Hyp	Ref	Expression
1		lnmlssfg.s	|- S = ( LSubSp ` M )
2		lnmlssfg.r	|- R = ( M |`s U )
3	1	islnm	|- ( M e. LNoeM <-> ( M e. LMod /\ A. a e. S ( M |`s a ) e. LFinGen ) )
4	3	simprbi	|- ( M e. LNoeM -> A. a e. S ( M |`s a ) e. LFinGen )
5		oveq2	|- ( a = U -> ( M |`s a ) = ( M |`s U ) )
6	5 2	eqtr4di	|- ( a = U -> ( M |`s a ) = R )
7	6	eleq1d	|- ( a = U -> ( ( M |`s a ) e. LFinGen <-> R e. LFinGen ) )
8	7	rspcv	|- ( U e. S -> ( A. a e. S ( M |`s a ) e. LFinGen -> R e. LFinGen ) )
9	4 8	mpan9	|- ( ( M e. LNoeM /\ U e. S ) -> R e. LFinGen )