lnmfg

Description: A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014)

		Ref	Expression
	Assertion	lnmfg	$⊢ M \in LNoeM \to M \in LFinGen$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{M} = {Base}_{M}$
2	1	ressid	$⊢ M \in LNoeM \to M ↾_{𝑠} {Base}_{M} = M$
3		lnmlmod	$⊢ M \in LNoeM \to M \in LMod$
4		eqid	$⊢ LSubSp (M) = LSubSp (M)$
5	1 4	lss1	$⊢ M \in LMod \to {Base}_{M} \in LSubSp (M)$
6	3 5	syl	$⊢ M \in LNoeM \to {Base}_{M} \in LSubSp (M)$
7		eqid	$⊢ M ↾_{𝑠} {Base}_{M} = M ↾_{𝑠} {Base}_{M}$
8	4 7	lnmlssfg	$⊢ (M \in LNoeM \land {Base}_{M} \in LSubSp (M)) \to M ↾_{𝑠} {Base}_{M} \in LFinGen$
9	6 8	mpdan	$⊢ M \in LNoeM \to M ↾_{𝑠} {Base}_{M} \in LFinGen$
10	2 9	eqeltrrd	$⊢ M \in LNoeM \to M \in LFinGen$

Metamath Proof Explorer