Metamath Proof Explorer


Theorem lnmlsslnm

Description: All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lnmlssfg.s S = LSubSp M
lnmlssfg.r R = M 𝑠 U
Assertion lnmlsslnm M LNoeM U S R LNoeM

Proof

Step Hyp Ref Expression
1 lnmlssfg.s S = LSubSp M
2 lnmlssfg.r R = M 𝑠 U
3 lnmlmod M LNoeM M LMod
4 2 1 lsslmod M LMod U S R LMod
5 3 4 sylan M LNoeM U S R LMod
6 2 oveq1i R 𝑠 a = M 𝑠 U 𝑠 a
7 simplr M LNoeM U S a LSubSp R U S
8 eqid Base R = Base R
9 eqid LSubSp R = LSubSp R
10 8 9 lssss a LSubSp R a Base R
11 10 adantl M LNoeM U S a LSubSp R a Base R
12 eqid Base M = Base M
13 12 1 lssss U S U Base M
14 2 12 ressbas2 U Base M U = Base R
15 13 14 syl U S U = Base R
16 15 ad2antlr M LNoeM U S a LSubSp R U = Base R
17 11 16 sseqtrrd M LNoeM U S a LSubSp R a U
18 ressabs U S a U M 𝑠 U 𝑠 a = M 𝑠 a
19 7 17 18 syl2anc M LNoeM U S a LSubSp R M 𝑠 U 𝑠 a = M 𝑠 a
20 6 19 syl5eq M LNoeM U S a LSubSp R R 𝑠 a = M 𝑠 a
21 simpll M LNoeM U S a LSubSp R M LNoeM
22 2 1 9 lsslss M LMod U S a LSubSp R a S a U
23 3 22 sylan M LNoeM U S a LSubSp R a S a U
24 23 simprbda M LNoeM U S a LSubSp R a S
25 eqid M 𝑠 a = M 𝑠 a
26 1 25 lnmlssfg M LNoeM a S M 𝑠 a LFinGen
27 21 24 26 syl2anc M LNoeM U S a LSubSp R M 𝑠 a LFinGen
28 20 27 eqeltrd M LNoeM U S a LSubSp R R 𝑠 a LFinGen
29 28 ralrimiva M LNoeM U S a LSubSp R R 𝑠 a LFinGen
30 9 islnm R LNoeM R LMod a LSubSp R R 𝑠 a LFinGen
31 5 29 30 sylanbrc M LNoeM U S R LNoeM