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 )