Metamath Proof Explorer

Theorem islnm

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

Ref Expression
Hypothesis islnm.s ⊢ S = LSubSp ⁡ M
Assertion islnm ⊢ M ∈ LNoeM ↔ M ∈ LMod ∧ ∀ i ∈ S M ↾ 𝑠 i ∈ LFinGen

Proof

Step Hyp Ref Expression
1 islnm.s ⊢ S = LSubSp ⁡ M
2 fveq2 ⊢ w = M → LSubSp ⁡ w = LSubSp ⁡ M
3 2 1 eqtr4di ⊢ w = M → LSubSp ⁡ w = S
4 oveq1 ⊢ w = M → w ↾ 𝑠 i = M ↾ 𝑠 i
5 4 eleq1d ⊢ w = M → w ↾ 𝑠 i ∈ LFinGen ↔ M ↾ 𝑠 i ∈ LFinGen
6 3 5 raleqbidv ⊢ w = M → ∀ i ∈ LSubSp ⁡ w w ↾ 𝑠 i ∈ LFinGen ↔ ∀ i ∈ S M ↾ 𝑠 i ∈ LFinGen
7 df-lnm ⊢ LNoeM = w ∈ LMod | ∀ i ∈ LSubSp ⁡ w w ↾ 𝑠 i ∈ LFinGen
8 6 7 elrab2 ⊢ M ∈ LNoeM ↔ M ∈ LMod ∧ ∀ i ∈ S M ↾ 𝑠 i ∈ LFinGen