Metamath Proof Explorer

Theorem 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 ∈ LNoeM ∧ U ∈ S → R ∈ LFinGen

Proof

Step Hyp Ref Expression
1 lnmlssfg.s ⊢ S = LSubSp ⁡ M
2 lnmlssfg.r ⊢ R = M ↾ 𝑠 U
3 1 islnm ⊢ M ∈ LNoeM ↔ M ∈ LMod ∧ ∀ a ∈ S M ↾ 𝑠 a ∈ LFinGen
4 3 simprbi ⊢ M ∈ LNoeM → ∀ a ∈ S M ↾ 𝑠 a ∈ LFinGen
5 oveq2 ⊢ a = U → M ↾ 𝑠 a = M ↾ 𝑠 U
6 5 2 eqtr4di ⊢ a = U → M ↾ 𝑠 a = R
7 6 eleq1d ⊢ a = U → M ↾ 𝑠 a ∈ LFinGen ↔ R ∈ LFinGen
8 7 rspcv ⊢ U ∈ S → ∀ a ∈ S M ↾ 𝑠 a ∈ LFinGen → R ∈ LFinGen
9 4 8 mpan9 ⊢ M ∈ LNoeM ∧ U ∈ S → R ∈ LFinGen