Theorem islnm

Description: Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014)

	Ref	Expression
Hypothesis	islnm.s	⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
Assertion	islnm	⊢ ( 𝑀 ∈ LNoeM ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑖 ∈ 𝑆 ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ) )

Proof

Step	Hyp	Ref	Expression
1		islnm.s	⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
2		fveq2	⊢ ( 𝑤 = 𝑀 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑀 ) )
3	2 1	eqtr4di	⊢ ( 𝑤 = 𝑀 → ( LSubSp ‘ 𝑤 ) = 𝑆 )
4		oveq1	⊢ ( 𝑤 = 𝑀 → ( 𝑤 ↾s 𝑖 ) = ( 𝑀 ↾s 𝑖 ) )
5	4	eleq1d	⊢ ( 𝑤 = 𝑀 → ( ( 𝑤 ↾s 𝑖 ) ∈ LFinGen ↔ ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ) )
6	3 5	raleqbidv	⊢ ( 𝑤 = 𝑀 → ( ∀ 𝑖 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑤 ↾s 𝑖 ) ∈ LFinGen ↔ ∀ 𝑖 ∈ 𝑆 ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ) )
7		df-lnm	⊢ LNoeM = { 𝑤 ∈ LMod ∣ ∀ 𝑖 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑤 ↾s 𝑖 ) ∈ LFinGen }
8	6 7	elrab2	⊢ ( 𝑀 ∈ LNoeM ↔ ( 𝑀 ∈ LMod ∧ ∀ 𝑖 ∈ 𝑆 ( 𝑀 ↾s 𝑖 ) ∈ LFinGen ) )