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=LSubSpM
lnmlssfg.r R=M𝑠U
Assertion lnmlsslnm MLNoeMUSRLNoeM

Proof

Step Hyp Ref Expression
1 lnmlssfg.s S=LSubSpM
2 lnmlssfg.r R=M𝑠U
3 lnmlmod MLNoeMMLMod
4 2 1 lsslmod MLModUSRLMod
5 3 4 sylan MLNoeMUSRLMod
6 2 oveq1i R𝑠a=M𝑠U𝑠a
7 simplr MLNoeMUSaLSubSpRUS
8 eqid BaseR=BaseR
9 eqid LSubSpR=LSubSpR
10 8 9 lssss aLSubSpRaBaseR
11 10 adantl MLNoeMUSaLSubSpRaBaseR
12 eqid BaseM=BaseM
13 12 1 lssss USUBaseM
14 2 12 ressbas2 UBaseMU=BaseR
15 13 14 syl USU=BaseR
16 15 ad2antlr MLNoeMUSaLSubSpRU=BaseR
17 11 16 sseqtrrd MLNoeMUSaLSubSpRaU
18 ressabs USaUM𝑠U𝑠a=M𝑠a
19 7 17 18 syl2anc MLNoeMUSaLSubSpRM𝑠U𝑠a=M𝑠a
20 6 19 eqtrid MLNoeMUSaLSubSpRR𝑠a=M𝑠a
21 simpll MLNoeMUSaLSubSpRMLNoeM
22 2 1 9 lsslss MLModUSaLSubSpRaSaU
23 3 22 sylan MLNoeMUSaLSubSpRaSaU
24 23 simprbda MLNoeMUSaLSubSpRaS
25 eqid M𝑠a=M𝑠a
26 1 25 lnmlssfg MLNoeMaSM𝑠aLFinGen
27 21 24 26 syl2anc MLNoeMUSaLSubSpRM𝑠aLFinGen
28 20 27 eqeltrd MLNoeMUSaLSubSpRR𝑠aLFinGen
29 28 ralrimiva MLNoeMUSaLSubSpRR𝑠aLFinGen
30 9 islnm RLNoeMRLModaLSubSpRR𝑠aLFinGen
31 5 29 30 sylanbrc MLNoeMUSRLNoeM