Theorem lnmlssfg

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

	Ref	Expression
Hypotheses	lnmlssfg.s	⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
	lnmlssfg.r	⊢ 𝑅 = ( 𝑀 ↾s 𝑈 )
Assertion	lnmlssfg	⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) → 𝑅 ∈ LFinGen )

Proof

Step	Hyp	Ref	Expression
1		lnmlssfg.s	⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
2		lnmlssfg.r	⊢ 𝑅 = ( 𝑀 ↾s 𝑈 )
3	1	islnm	⊢ ( 𝑀 ∈ LNoeM ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑎 ∈ 𝑆 ( 𝑀 ↾s 𝑎 ) ∈ LFinGen ) )
4	3	simprbi	⊢ ( 𝑀 ∈ LNoeM → ∀ 𝑎 ∈ 𝑆 ( 𝑀 ↾s 𝑎 ) ∈ LFinGen )
5		oveq2	⊢ ( 𝑎 = 𝑈 → ( 𝑀 ↾s 𝑎 ) = ( 𝑀 ↾s 𝑈 ) )
6	5 2	eqtr4di	⊢ ( 𝑎 = 𝑈 → ( 𝑀 ↾s 𝑎 ) = 𝑅 )
7	6	eleq1d	⊢ ( 𝑎 = 𝑈 → ( ( 𝑀 ↾s 𝑎 ) ∈ LFinGen ↔ 𝑅 ∈ LFinGen ) )
8	7	rspcv	⊢ ( 𝑈 ∈ 𝑆 → ( ∀ 𝑎 ∈ 𝑆 ( 𝑀 ↾s 𝑎 ) ∈ LFinGen → 𝑅 ∈ LFinGen ) )
9	4 8	mpan9	⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) → 𝑅 ∈ LFinGen )