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 
|- S = ( Scalar ` M )
Assertion lnrfg 
|- ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM )

Proof

Step Hyp Ref Expression
1 lnrfg.s 
 |-  S = ( Scalar ` M )
2 eqid 
 |-  ( S freeLMod a ) = ( S freeLMod a )
3 eqid 
 |-  ( Base ` ( S freeLMod a ) ) = ( Base ` ( S freeLMod a ) )
4 eqid 
 |-  ( Base ` M ) = ( Base ` M )
5 eqid 
 |-  ( .s ` M ) = ( .s ` M )
6 eqid 
 |-  ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) )
7 fglmod 
 |-  ( M e. LFinGen -> M e. LMod )
8 7 ad3antrrr 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> M e. LMod )
9 vex 
 |-  a e. _V
10 9 a1i 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> a e. _V )
11 1 a1i 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> S = ( Scalar ` M ) )
12 f1oi 
 |-  ( _I |` a ) : a -1-1-onto-> a
13 f1of 
 |-  ( ( _I |` a ) : a -1-1-onto-> a -> ( _I |` a ) : a --> a )
14 12 13 ax-mp 
 |-  ( _I |` a ) : a --> a
15 elpwi 
 |-  ( a e. ~P ( Base ` M ) -> a C_ ( Base ` M ) )
16 fss 
 |-  ( ( ( _I |` a ) : a --> a /\ a C_ ( Base ` M ) ) -> ( _I |` a ) : a --> ( Base ` M ) )
17 14 15 16 sylancr 
 |-  ( a e. ~P ( Base ` M ) -> ( _I |` a ) : a --> ( Base ` M ) )
18 17 ad2antlr 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( _I |` a ) : a --> ( Base ` M ) )
19 2 3 4 5 6 8 10 11 18 frlmup1 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) e. ( ( S freeLMod a ) LMHom M ) )
20 simpllr 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> S e. LNoeR )
21 simprl 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> a e. Fin )
22 2 lnrfrlm 
 |-  ( ( S e. LNoeR /\ a e. Fin ) -> ( S freeLMod a ) e. LNoeM )
23 20 21 22 syl2anc 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( S freeLMod a ) e. LNoeM )
24 eqid 
 |-  ( LSpan ` M ) = ( LSpan ` M )
25 2 3 4 5 6 8 10 11 18 24 frlmup3 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( ( LSpan ` M ) ` ran ( _I |` a ) ) )
26 rnresi 
 |-  ran ( _I |` a ) = a
27 26 fveq2i 
 |-  ( ( LSpan ` M ) ` ran ( _I |` a ) ) = ( ( LSpan ` M ) ` a )
28 simprr 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( ( LSpan ` M ) ` a ) = ( Base ` M ) )
29 27 28 eqtrid 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( ( LSpan ` M ) ` ran ( _I |` a ) ) = ( Base ` M ) )
30 25 29 eqtrd 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( Base ` M ) )
31 4 lnmepi 
 |-  ( ( ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) e. ( ( S freeLMod a ) LMHom M ) /\ ( S freeLMod a ) e. LNoeM /\ ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( Base ` M ) ) -> M e. LNoeM )
32 19 23 30 31 syl3anc 
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> M e. LNoeM )
33 4 24 islmodfg 
 |-  ( M e. LMod -> ( M e. LFinGen <-> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) )
34 7 33 syl 
 |-  ( M e. LFinGen -> ( M e. LFinGen <-> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) )
35 34 ibi 
 |-  ( M e. LFinGen -> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) )
36 35 adantr 
 |-  ( ( M e. LFinGen /\ S e. LNoeR ) -> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) )
37 32 36 r19.29a 
 |-  ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM )