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 = Scalar (M)$
	lnrfgtr.u	$⊢ U = LSubSp (M)$
	lnrfgtr.n	$⊢ N = M ↾_{𝑠} P$
Assertion	lnrfgtr	$⊢ (M \in LFinGen \land S \in LNoeR \land P \in U) \to N \in LFinGen$

Proof

Step	Hyp	Ref	Expression
1		lnrfg.s	$⊢ S = Scalar (M)$
2		lnrfgtr.u	$⊢ U = LSubSp (M)$
3		lnrfgtr.n	$⊢ N = M ↾_{𝑠} P$
4	1	lnrfg	$⊢ (M \in LFinGen \land S \in LNoeR) \to M \in LNoeM$
5	2 3	lnmlssfg	$⊢ (M \in LNoeM \land P \in U) \to N \in LFinGen$
6	4 5	stoic3	$⊢ (M \in LFinGen \land S \in LNoeR \land P \in U) \to N \in LFinGen$