Description: All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lnmlssfg.s | |
|
lnmlssfg.r | |
||
Assertion | lnmlsslnm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lnmlssfg.s | |
|
2 | lnmlssfg.r | |
|
3 | lnmlmod | |
|
4 | 2 1 | lsslmod | |
5 | 3 4 | sylan | |
6 | 2 | oveq1i | |
7 | simplr | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | 8 9 | lssss | |
11 | 10 | adantl | |
12 | eqid | |
|
13 | 12 1 | lssss | |
14 | 2 12 | ressbas2 | |
15 | 13 14 | syl | |
16 | 15 | ad2antlr | |
17 | 11 16 | sseqtrrd | |
18 | ressabs | |
|
19 | 7 17 18 | syl2anc | |
20 | 6 19 | eqtrid | |
21 | simpll | |
|
22 | 2 1 9 | lsslss | |
23 | 3 22 | sylan | |
24 | 23 | simprbda | |
25 | eqid | |
|
26 | 1 25 | lnmlssfg | |
27 | 21 24 26 | syl2anc | |
28 | 20 27 | eqeltrd | |
29 | 28 | ralrimiva | |
30 | 9 | islnm | |
31 | 5 29 30 | sylanbrc | |