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 ↾_{𝑠} U$
Assertion	lnmlssfg	$⊢ (M \in LNoeM \land U \in S) \to R \in LFinGen$

Step	Hyp	Ref	Expression
1		lnmlssfg.s	$⊢ S = LSubSp (M)$
2		lnmlssfg.r	$⊢ R = M ↾_{𝑠} U$
3	1	islnm	$⊢ M \in LNoeM \leftrightarrow (M \in LMod \land \forall a \in S M ↾_{𝑠} a \in LFinGen)$
4	3	simprbi	$⊢ M \in LNoeM \to \forall a \in S M ↾_{𝑠} a \in LFinGen$
5		oveq2	$⊢ a = U \to M ↾_{𝑠} a = M ↾_{𝑠} U$
6	5 2	eqtr4di	$⊢ a = U \to M ↾_{𝑠} a = R$
7	6	eleq1d	$⊢ a = U \to (M ↾_{𝑠} a \in LFinGen \leftrightarrow R \in LFinGen)$
8	7	rspcv	$⊢ U \in S \to (\forall a \in S M ↾_{𝑠} a \in LFinGen \to R \in LFinGen)$
9	4 8	mpan9	$⊢ (M \in LNoeM \land U \in S) \to R \in LFinGen$

Metamath Proof Explorer