Metamath Proof Explorer

Theorem lnrfg

Description: Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015)

Ref Expression
Hypothesis lnrfg.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
Assertion lnrfg ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → 𝑀 ∈ LNoeM )

Proof

Step Hyp Ref Expression
1 lnrfg.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
2 eqid ⊢ ( 𝑆 freeLMod 𝑎 ) = ( 𝑆 freeLMod 𝑎 )
3 eqid ⊢ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) = ( Base ‘ ( 𝑆 freeLMod 𝑎 ) )
4 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
6 eqid ⊢ ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) )
7 fglmod ⊢ ( 𝑀 ∈ LFinGen → 𝑀 ∈ LMod )
8 7 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod )
9 vex ⊢ 𝑎 ∈ V
10 9 a1i ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑎 ∈ V )
11 1 a1i ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑆 = ( Scalar ‘ 𝑀 ) )
12 f1oi ⊢ ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎
13 f1of ⊢ ( ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎 → ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎 )
14 12 13 ax-mp ⊢ ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎
15 elpwi ⊢ ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) → 𝑎 ⊆ ( Base ‘ 𝑀 ) )
16 fss ⊢ ( ( ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎 ∧ 𝑎 ⊆ ( Base ‘ 𝑀 ) ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) )
17 14 15 16 sylancr ⊢ ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) )
18 17 ad2antlr ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) )
19 2 3 4 5 6 8 10 11 18 frlmup1 ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) ∈ ( ( 𝑆 freeLMod 𝑎 ) LMHom 𝑀 ) )
20 simpllr ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑆 ∈ LNoeR )
21 simprl ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑎 ∈ Fin )
22 2 lnrfrlm ⊢ ( ( 𝑆 ∈ LNoeR ∧ 𝑎 ∈ Fin ) → ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM )
23 20 21 22 syl2anc ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM )
24 eqid ⊢ ( LSpan ‘ 𝑀 ) = ( LSpan ‘ 𝑀 )
25 2 3 4 5 6 8 10 11 18 24 frlmup3 ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) )
26 rnresi ⊢ ran ( I ↾ 𝑎 ) = 𝑎
27 26 fveq2i ⊢ ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) = ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 )
28 simprr ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) )
29 27 28 syl5eq ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) = ( Base ‘ 𝑀 ) )
30 25 29 eqtrd ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( Base ‘ 𝑀 ) )
31 4 lnmepi ⊢ ( ( ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) ∈ ( ( 𝑆 freeLMod 𝑎 ) LMHom 𝑀 ) ∧ ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM ∧ ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( Base ‘ 𝑀 ) ) → 𝑀 ∈ LNoeM )
32 19 23 30 31 syl3anc ⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LNoeM )
33 4 24 islmodfg ⊢ ( 𝑀 ∈ LMod → ( 𝑀 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) )
34 7 33 syl ⊢ ( 𝑀 ∈ LFinGen → ( 𝑀 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) )
35 34 ibi ⊢ ( 𝑀 ∈ LFinGen → ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) )
36 35 adantr ⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) )
37 32 36 r19.29a ⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → 𝑀 ∈ LNoeM )