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 |`s U )
Assertion lnmlsslnm 
|- ( ( M e. LNoeM /\ U e. S ) -> R e. LNoeM )

Proof

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