Theorem lnmfg

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

	Ref	Expression
Assertion	lnmfg	⊢ ( 𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
2	1	ressid	⊢ ( 𝑀 ∈ LNoeM → ( 𝑀 ↾s ( Base ‘ 𝑀 ) ) = 𝑀 )
3		lnmlmod	⊢ ( 𝑀 ∈ LNoeM → 𝑀 ∈ LMod )
4		eqid	⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
5	1 4	lss1	⊢ ( 𝑀 ∈ LMod → ( Base ‘ 𝑀 ) ∈ ( LSubSp ‘ 𝑀 ) )
6	3 5	syl	⊢ ( 𝑀 ∈ LNoeM → ( Base ‘ 𝑀 ) ∈ ( LSubSp ‘ 𝑀 ) )
7		eqid	⊢ ( 𝑀 ↾s ( Base ‘ 𝑀 ) ) = ( 𝑀 ↾s ( Base ‘ 𝑀 ) )
8	4 7	lnmlssfg	⊢ ( ( 𝑀 ∈ LNoeM ∧ ( Base ‘ 𝑀 ) ∈ ( LSubSp ‘ 𝑀 ) ) → ( 𝑀 ↾s ( Base ‘ 𝑀 ) ) ∈ LFinGen )
9	6 8	mpdan	⊢ ( 𝑀 ∈ LNoeM → ( 𝑀 ↾s ( Base ‘ 𝑀 ) ) ∈ LFinGen )
10	2 9	eqeltrrd	⊢ ( 𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen )