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 ⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
lnmlssfg.r ⊢ 𝑅 = ( 𝑀 ↾s 𝑈 )
Assertion lnmlsslnm ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) → 𝑅 ∈ LNoeM )

Proof

Step Hyp Ref Expression
1 lnmlssfg.s ⊢ 𝑆 = ( LSubSp ‘ 𝑀 )
2 lnmlssfg.r ⊢ 𝑅 = ( 𝑀 ↾s 𝑈 )
3 lnmlmod ⊢ ( 𝑀 ∈ LNoeM → 𝑀 ∈ LMod )
4 2 1 lsslmod ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑅 ∈ LMod )
5 3 4 sylan ⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) → 𝑅 ∈ LMod )
6 2 oveq1i ⊢ ( 𝑅 ↾s 𝑎 ) = ( ( 𝑀 ↾s 𝑈 ) ↾s 𝑎 )
7 simplr ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → 𝑈 ∈ 𝑆 )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( LSubSp ‘ 𝑅 ) = ( LSubSp ‘ 𝑅 )
10 8 9 lssss ⊢ ( 𝑎 ∈ ( LSubSp ‘ 𝑅 ) → 𝑎 ⊆ ( Base ‘ 𝑅 ) )
11 10 adantl ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → 𝑎 ⊆ ( Base ‘ 𝑅 ) )
12 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
13 12 1 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑀 ) )
14 2 12 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝑀 ) → 𝑈 = ( Base ‘ 𝑅 ) )
15 13 14 syl ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 = ( Base ‘ 𝑅 ) )
16 15 ad2antlr ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → 𝑈 = ( Base ‘ 𝑅 ) )
17 11 16 sseqtrrd ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → 𝑎 ⊆ 𝑈 )
18 ressabs ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑎 ⊆ 𝑈 ) → ( ( 𝑀 ↾s 𝑈 ) ↾s 𝑎 ) = ( 𝑀 ↾s 𝑎 ) )
19 7 17 18 syl2anc ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → ( ( 𝑀 ↾s 𝑈 ) ↾s 𝑎 ) = ( 𝑀 ↾s 𝑎 ) )
20 6 19 eqtrid ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑎 ) = ( 𝑀 ↾s 𝑎 ) )
21 simpll ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → 𝑀 ∈ LNoeM )
22 2 1 9 lsslss ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ↔ ( 𝑎 ∈ 𝑆 ∧ 𝑎 ⊆ 𝑈 ) ) )
23 3 22 sylan ⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) → ( 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ↔ ( 𝑎 ∈ 𝑆 ∧ 𝑎 ⊆ 𝑈 ) ) )
24 23 simprbda ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → 𝑎 ∈ 𝑆 )
25 eqid ⊢ ( 𝑀 ↾s 𝑎 ) = ( 𝑀 ↾s 𝑎 )
26 1 25 lnmlssfg ⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ↾s 𝑎 ) ∈ LFinGen )
27 21 24 26 syl2anc ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → ( 𝑀 ↾s 𝑎 ) ∈ LFinGen )
28 20 27 eqeltrd ⊢ ( ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑎 ) ∈ LFinGen )
29 28 ralrimiva ⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) → ∀ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ( 𝑅 ↾s 𝑎 ) ∈ LFinGen )
30 9 islnm ⊢ ( 𝑅 ∈ LNoeM ↔ ( 𝑅 ∈ LMod ∧ ∀ 𝑎 ∈ ( LSubSp ‘ 𝑅 ) ( 𝑅 ↾s 𝑎 ) ∈ LFinGen ) )
31 5 29 30 sylanbrc ⊢ ( ( 𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆 ) → 𝑅 ∈ LNoeM )