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	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	lnrfgtr.u	⊢ 𝑈 = ( LSubSp ‘ 𝑀 )
	lnrfgtr.n	⊢ 𝑁 = ( 𝑀 ↾s 𝑃 )
Assertion	lnrfgtr	⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ∧ 𝑃 ∈ 𝑈 ) → 𝑁 ∈ LFinGen )

Proof

Step	Hyp	Ref	Expression
1		lnrfg.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
2		lnrfgtr.u	⊢ 𝑈 = ( LSubSp ‘ 𝑀 )
3		lnrfgtr.n	⊢ 𝑁 = ( 𝑀 ↾s 𝑃 )
4	1	lnrfg	⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → 𝑀 ∈ LNoeM )
5	2 3	lnmlssfg	⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑃 ∈ 𝑈 ) → 𝑁 ∈ LFinGen )
6	4 5	stoic3	⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ∧ 𝑃 ∈ 𝑈 ) → 𝑁 ∈ LFinGen )